/share-insight
Draft a shareable insight from your session as a GitHub issue
> /plugin marketplace add cameronfreer/lean4-skillsHow it fires
How this command gets triggered: by you, by Claude, or both.
- Fires itselfClaude auto-loads it when your prompt matches the work.
- You can call itInvoke it directly when you want it.
- Slash command
/share-insight
Context preview
What this command does when you run it.
Draft a shareable insight from your session as a GitHub issue
Command definition
share-insight.mdname: share-insight
description: Draft a shareable insight from your session as a GitHub issue
Share Insight
Draft and submit a reusable insight (pattern, antipattern, or mixed) as a GitHub issue on `cameronfreer/lean4-skills`.
Precondition
Invoke this command only if the user explicitly ran it or explicitly agreed to draft a shareable insight. If invoked without prior opt-in, ask:
> That seems reusable beyond this task. Want me to draft a shareable insight?
If the user explicitly ran `/lean4-contribute:share-insight`, treat that as opt-in. Do not proceed unless the user confirms. Do not mine git diff, infer insight candidates, or ask structured questions until consent is given.
Discovering Candidates
Once the user has opted in (see [Precondition](#precondition) above), look at:
- Current conversation / session context
- Current git diff (`git diff` and `git diff --cached`)
- Recently touched `.lean` files
From these, infer **1–5 candidate insights**. For each candidate, note:
- A one-line title (keep titles generic — avoid project-specific names, paths, or identifiers)
- Classification: **pattern** (what worked), **antipattern** (what failed), or
**mixed** (worked in some contexts, failed in others)
Present the candidates as a numbered list and ask the user to pick one (or describe a different insight). Proceed with the selected insight.
Gathering Context
For the chosen insight, collect or infer:
1. **Kind** — pattern / antipattern / mixed 2. **Title** — Concise, descriptive title 3. **Context** — What were you working on when you discovered this? 4. **Symptom / trigger** — What behavior or error led to the discovery? 5. **What worked / what failed** — The core lesson 6. **Why it matters** — Impact on proving, performance, readability, or correctness 7. **Minimal example** — Smallest Lean snippet illustrating the insight (strip project-specific details) 8. **When to use / when not to** — Applicability boundaries 9. **Confidence** — High / medium / low — how sure are you this generalizes? 10. **Privacy / redaction check** — Scan for filesystem paths, usernames, API keys, or other sensitive data and redact them. Flag anything you redacted so the user can verify.
Drafting the Issue
Compose the issue using this template:
Title: [Insight] <title>
Labels: insight
## Kind
<pattern / antipattern / mixed>
## Context
<what you were working on>
## Symptom / Trigger
<behavior or error that led to discovery>
## What Worked / What Failed
<core lesson>
## Why It Matters
<impact>
## Minimal Example
```lean
<minimal Lean snippet>
When to Use / When Not To
<applicability boundaries>
Confidence
<high / medium / low>
--- *Drafted via [lean4-contribute](https://github.com/cameronfreer/lean4-skills)*
## Showing the Draft
Display the **complete** issue draft to the user — title, labels, and full body.
Also list any alternate candidates that were not selected, in case the user
wants to switch. Ask:
> Here is the insight I will submit. Review it carefully — it may contain code
> snippets from your session.
>
> By submitting, you agree that this content may be edited, rearranged, or
> incorporated into lean4-skills in any form under its
> [MIT license](https://github.com/cameronfreer/lean4-skills/blob/main/LICENSE).
>
> **Submit this issue?** (yes / edit / switch to alternate / cancel)
Do **not** proceed unless the user explicitly confirms.
## Submitting
After confirmation, submit using the first available method:
1. **`gh` CLI** — Try: `gh issue create --repo cameronfreer/lean4-skills --title "<title>" --body "<body>" --label insight`.
If the label fails (e.g. `insight` doesn't exist on the repo), retry without
`--label` and note that the label was advisory only.
If `gh` fails for auth or network reasons, **stop** — do not retry. Fall
through to the browser or email path immediately.
2. **Browser fallback** — Provide a prefilled GitHub URL:
`https://github.com/cameronfreer/lean4-skills/issues/new?title=<url-encoded-title>&body=<url-encoded-body>&labels=insight`
(the `labels=` param is best-effort; GitHub ignores unknown labels silently)
3. **Email fallback** — Draft an email to `lean4skills@gmail.com` with subject
`[Insight] <title>` and the full issue body, for the user to send manually.
Report the result (issue URL, fallback URL, or email draft) and confirm
completion.
Read more
name: share-insight description: Draft a shareable insight from your session as a GitHub issue
Share Insight
Draft and submit a reusable insight (pattern, antipattern, or mixed) as a GitHub issue on `cameronfreer/lean4-skills`.
Precondition
Invoke this command only if the user explicitly ran it or explicitly agreed to draft a shareable insight. If invoked without prior opt-in, ask:
> That seems reusable beyond this task. Want me to draft a shareable insight?
If the user explicitly ran `/lean4-contribute:share-insight`, treat that as opt-in. Do not proceed unless the user confirms. Do not mine git diff, infer insight candidates, or ask structured questions until consent is given.
Discovering Candidates
Once the user has opted in (see [Precondition](#precondition) above), look at:
- Current conversation / session context
- Current git diff (`git diff` and `git diff --cached`)
- Recently touched `.lean` files
From these, infer **1–5 candidate insights**. For each candidate, note:
- A one-line title (keep titles generic — avoid project-specific names, paths, or identifiers)
- Classification: **pattern** (what worked), **antipattern** (what failed), or
**mixed** (worked in some contexts, failed in others)
Present the candidates as a numbered list and ask the user to pick one (or describe a different insight). Proceed with the selected insight.
Gathering Context
For the chosen insight, collect or infer:
1. **Kind** — pattern / antipattern / mixed 2. **Title** — Concise, descriptive title 3. **Context** — What were you working on when you discovered this? 4. **Symptom / trigger** — What behavior or error led to the discovery? 5. **What worked / what failed** — The core lesson 6. **Why it matters** — Impact on proving, performance, readability, or correctness 7. **Minimal example** — Smallest Lean snippet illustrating the insight (strip project-specific details) 8. **When to use / when not to** — Applicability boundaries 9. **Confidence** — High / medium / low — how sure are you this generalizes? 10. **Privacy / redaction check** — Scan for filesystem paths, usernames, API keys, or other sensitive data and redact them. Flag anything you redacted so the user can verify.
Drafting the Issue
Compose the issue using this template:
Title: [Insight] <title> Labels: insight ## Kind <pattern / antipattern / mixed> ## Context <what you were working on> ## Symptom / Trigger <behavior or error that led to discovery> ## What Worked / What Failed <core lesson> ## Why It Matters <impact> ## Minimal Example ```lean <minimal Lean snippet>
When to Use / When Not To
<applicability boundaries>
Confidence
<high / medium / low>
--- *Drafted via [lean4-contribute](https://github.com/cameronfreer/lean4-skills)*
## Showing the Draft Display the **complete** issue draft to the user — title, labels, and full body. Also list any alternate candidates that were not selected, in case the user wants to switch. Ask: > Here is the insight I will submit. Review it carefully — it may contain code > snippets from your session. > > By submitting, you agree that this content may be edited, rearranged, or > incorporated into lean4-skills in any form under its > [MIT license](https://github.com/cameronfreer/lean4-skills/blob/main/LICENSE). > > **Submit this issue?** (yes / edit / switch to alternate / cancel) Do **not** proceed unless the user explicitly confirms. ## Submitting After confirmation, submit using the first available method: 1. **`gh` CLI** — Try: `gh issue create --repo cameronfreer/lean4-skills --title "<title>" --body "<body>" --label insight`. If the label fails (e.g. `insight` doesn't exist on the repo), retry without `--label` and note that the label was advisory only. If `gh` fails for auth or network reasons, **stop** — do not retry. Fall through to the browser or email path immediately. 2. **Browser fallback** — Provide a prefilled GitHub URL: `https://github.com/cameronfreer/lean4-skills/issues/new?title=<url-encoded-title>&body=<url-encoded-body>&labels=insight` (the `labels=` param is best-effort; GitHub ignores unknown labels silently) 3. **Email fallback** — Draft an email to `lean4skills@gmail.com` with subject `[Insight] <title>` and the full issue body, for the user to send manually. Report the result (issue URL, fallback URL, or email draft) and confirm completion.
Lean 4 workflow pack for AI coding agents. Gives your agent a structured prove/review/golf loop, mathlib search, axiom checking, and safety guardrails.
Other commands on lean4-skills.
- /bug-report
Draft a bug report issue for lean4-skills
Open command - /feature-request
Draft a feature request issue for lean4-skills
Open command - /autoformalize
Autonomous end-to-end formalization from informal sources
Open command - /autoprove
Autonomous multi-cycle theorem proving with explicit stop budgets
Open command - /checkpoint
Save progress with a safe commit checkpoint
Open command - /diagnose
Diagnostics, cleanup, and migration help
Open command