lean4-prove
Retrieval-augmented Lean4 proof generation. Queries 94k+ exemplars from DeepSeek-Prover V1+V2, uses hybrid search (BM25 + semantic + graph), generates via Claude, compiles in Docker, retries on failure.
npx skills add majiayu000/claude-skill-registry --skill lean4-prove --agent claude-code
Same command for any agent — swap --agent for codex, cursor, copilot.
Weekly change comes from our own snapshots, not the repository page — it measures attention, not adoption.
# lean4-prove Retrieval-augmented Lean4 proof generation for engineering requirements. Uses 94,000+ proven theorems from DeepSeek-Prover V1+V2 to guide proof synthesis via hybrid search (BM25 + semantic + graph traversal). ## Architecture ``` Requirement + Tactics + Persona │ ▼ ┌───────────────────────────┐ │ 1. RECALL similar proofs │ ← Hybrid search on ArangoDB │ from 94k+ exemplars │ (BM25 + semantic + graph) └───────────────────────────┘ │ ▼ ┌───────────────────────────┐ │ 2. BUILD support pack │ │ - Validated imports │ │ - Tactic patterns │ │ - Similar proofs │ └───────────────────────────┘ │ ▼ ┌───────────────────────────┐ │ 3. GENERATE N candidates │ ← Claude with exemplar context │ constrained by corpus │ └───────────────────────────┘ │ ▼ ┌───────────────────────────┐ │ 4. COMPILE each in │ ← lean_runner Docker │ lean_runner container │ └───────────────────────────┘ │ ┌────┴────┐ │ │ Success Failure │ │ ▼ ▼ Return Retry with error feedback (up to max_retries) ``` ## Why Retrieval-Augmented? 1. **Determinism** - Exact provenance: "used these 3 proofs as templates" 2. **Version alignment** - Exemplars use imports that actually work 3. **Fewer hallucinations** - Constrained to
- Architecture
- Why Retrieval-Augmented?
- Usage
- Output
- Parameters
- Environment Variables
- Dataset Setup
- Authentication
- Requirements
- Tactics
- Examples
- Engineering: List operations
- Engineering: State machine property
- Engineering: Protocol correctness
Basic proof
With tactics preference
With persona context
Via stdin (JSON)
echo '{"requirement": "Prove n + 0 = n", "tactics": ["rfl"]}' | ./run.sh
Custom settings
Proof generation
Retrieval (requires ArangoDB with ingested dataset)
Ingest full dataset (~5 min)
Or limit for testingWhat does the lean4-prove skill do?
Retrieval-augmented Lean4 proof generation. Queries 94k+ exemplars from DeepSeek-Prover V1+V2, uses hybrid search (BM25 + semantic + graph), generates via Claude, compiles in Docker, retries on failure.
How do I install it?
Run `npx skills add majiayu000/claude-skill-registry --skill lean4-prove --agent claude-code` — it drops the skill into your project so the agent can pick it up. Swap the --agent value for codex, cursor or copilot if you use one of those.
Where does this skill come from?
From majiayu000/claude-skill-registry, a repository with 534 stars. We read it straight from the repository tree rather than a submitted listing, so what you see here is what is actually published.
Is a popular skill a good skill?
Not necessarily. Stars measure attention, not adoption — a repository can trend for a week and be abandoned. That is why we show the weekly change from our own snapshots next to the total, instead of a single flattering number.