lean-formalize
Develop and verify a mathematical proof in Lean, continue an incomplete Lean project, or audit whether it proves the original statement. Connect actual inputs to intermediate lemmas, assemble the target theorem, check its transitive axioms, and provide a reproducible handoff. Use when Lean is requested or a specific proof obligation benefits from formal verification; use proof-writer for ordinary...
| Field | Value |
|---|---|
| Owner | wanshuiyin |
| Curator | Thomas Cherickal |
| Source | wanshuiyin/Auto-claude-code-research-in-sleep |
| Repo stars | 19,200 |
| License | MIT |
| Repo last push | 2026-11-14 |
Links
- Roles: quantum-computing-researcher
- Source repo: wanshuiyin/Auto-claude-code-research-in-sleep
- Same repo: render-html, mermaid-diagram, specification-writing, ablation-planner, arxiv, experiment-plan, novelty-check, openalex
- Registry seed skills for this role: quantum-computing-researcher seed skills