Add Claude Code skill and AI Agents docs section

Gabrielebattimelli · Gabrielebattimelli · commit 944f2947669c · 2026-04-22T20:42:32.000+02:00
diff --git a/.claude/skills/physlibsearch/SKILL.md b/.claude/skills/physlibsearch/SKILL.md
@@ -0,0 +1,249 @@
+---
+name: physlibsearch
+description: Semantic search over Physlib, a formal Lean 4 library of physics theorems and definitions. Use when asked to find Lean 4 declarations related to physics or mathematics, look up formal proofs, retrieve theorem signatures, or browse the Physlib module hierarchy.
+---
+
+# PhyslibSearch API Skill
+
+PhyslibSearch is a semantic search engine over **Physlib**, a Lean 4 formal library of physics and mathematics. It lets you find theorems, definitions, lemmas, and instances by describing them in natural language — no Lean syntax required.
+
+**Base URL**: `https://physlibsearch.net`
+
+---
+
+## When to use this skill
+
+- The user asks to find a Lean 4 theorem, definition, or proof about a physics/math concept.
+- The user wants the formal statement (signature) of a known result (e.g. Newton's second law, Schrödinger equation).
+- The user wants to browse what Physlib covers in a specific area.
+- The user has a Lean 4 declaration name and wants its full record.
+
+---
+
+## Endpoints
+
+### 1. Search — `POST /search`
+
+The main endpoint. Submit one or more natural language queries, get ranked results.
+
+**Request**
+```json
+{
+  "query": ["Newton's second law"],
+  "num_results": 10
+}
+```
+- `query`: array of strings (1–many queries); each runs independently and returns its own ranked list.
+- `num_results`: 1–150, default 10.
+
+**Response** — `list[list[QueryResult]]` (one list per query, ordered by relevance)
+```json
+[[
+  {
+    "result": {
+      "module_name": ["Physlib", "Mechanics", "Newton"],
+      "kind": "theorem",
+      "name": ["Physlib", "Mechanics", "Newton", "secondLaw"],
+      "signature": "theorem Physlib.Mechanics.Newton.secondLaw : ∀ (m F : ℝ), m > 0 → acceleration m F = F / m",
+      "type": "Prop",
+      "value": null,
+      "docstring": null,
+      "informal_name": "Newton's Second Law",
+      "informal_description": "For a body of mass $m > 0$ and applied force $F$, the acceleration satisfies $a = F/m$."
+    },
+    "distance": 0.12
+  }
+]]
+```
+
+**Key fields**:
+- `distance` — cosine distance (lower = more relevant; 0 is perfect).
+- `informal_name` / `informal_description` — human-readable explanation (LaTeX math).
+- `signature` — the formal Lean 4 statement.
+- `name` — fully-qualified name as a string array (use with `/fetch`).
+- `kind` — `theorem`, `definition`, `lemma`, `instance`, `axiom`, etc.
+
+**Example (curl)**
+```bash
+curl -s -X POST https://physlibsearch.net/search \
+  -H "Content-Type: application/json" \
+  -d '{"query": ["quantum harmonic oscillator energy levels"], "num_results": 5}'
+```
+
+---
+
+### 2. Query Expansion — `POST /expand`
+
+Optionally call this **before** `/search` to improve results for technical or ambiguous queries. It uses HyDE (Hypothetical Document Embeddings): Gemini generates a plausible hypothetical Lean declaration, which is then used as the search vector.
+
+**Request** — raw JSON string (the query itself, not an object)
+```json
+"Schrödinger equation for a free particle"
+```
+
+**Response** — JSON string (expanded query or original on failure)
+```json
+"theorem Physlib.QuantumMechanics.FreeParticle.schrodinger : ..."
+```
+
+**When to use**: For precise or highly technical queries (specific equation names, less common concepts). For broad natural-language queries, go straight to `/search`.
+
+**Example flow**
+```bash
+# Step 1: expand
+EXPANDED=$(curl -s -X POST https://physlibsearch.net/expand \
+  -H "Content-Type: application/json" \
+  -d '"Schrödinger equation for a free particle"')
+
+# Step 2: search with expanded query
+curl -s -X POST https://physlibsearch.net/search \
+  -H "Content-Type: application/json" \
+  -d "{\"query\": [$EXPANDED], \"num_results\": 5}"
+```
+
+---
+
+### 3. Fetch by Name — `POST /fetch`
+
+Retrieve full records for known Lean declaration names. Use this when you already have a name from a prior search or from the user.
+
+**Request**
+```json
+{
+  "query": [
+    ["Physlib", "Mechanics", "Newton", "secondLaw"],
+    ["Physlib", "QuantumMechanics", "HarmonicOscillator", "energy"]
+  ]
+}
+```
+- Each entry is a `LeanName` — an array of strings forming the fully-qualified path.
+
+**Response** — `list[Record | null]` (null for names not found, order preserved)
+
+**Example (curl)**
+```bash
+curl -s -X POST https://physlibsearch.net/fetch \
+  -H "Content-Type: application/json" \
+  -d '{"query": [["Physlib", "Mechanics", "Newton", "secondLaw"]]}'
+```
+
+---
+
+### 4. List Modules — `GET /modules`
+
+Returns all top-level Physlib modules with a count of searchable declarations.
+
+**Response**
+```json
+[
+  {"name": ["Physlib", "Mechanics"], "count": 42},
+  {"name": ["Physlib", "QuantumMechanics"], "count": 31}
+]
+```
+
+**Example (curl)**
+```bash
+curl -s https://physlibsearch.net/modules
+```
+
+---
+
+### 5. Module Declarations — `POST /modules/declarations`
+
+Returns all declarations in a specific module, ordered by source position.
+
+**Request** — raw JSON array (the module name, not wrapped in an object)
+```json
+["Physlib", "Mechanics", "Newton"]
+```
+
+**Response** — `list[Record]` (same shape as search results, without `distance`)
+
+**Example (curl)**
+```bash
+curl -s -X POST https://physlibsearch.net/modules/declarations \
+  -H "Content-Type: application/json" \
+  -d '["Physlib", "Mechanics", "Newton"]'
+```
+
+---
+
+## Best practices
+
+### Write queries like you'd explain the concept to a physicist, not like Lean code
+
+| Good | Avoid |
+|------|-------|
+| `"conservation of momentum"` | `"theorem momentum"` |
+| `"energy of a quantum harmonic oscillator"` | `"E_n = hbar omega (n + 1/2)"` |
+| `"Maxwell's equations in differential form"` | `"curl E = -dB/dt"` |
+| `"Euler-Lagrange equation"` | `"Lagrangian mechanics derivative"` |
+
+### Batch multiple queries in one request
+
+If you need to answer several related questions, send them together — each gets its own ranked list and it's a single round trip:
+```json
+{
+  "query": [
+    "kinetic energy theorem",
+    "work-energy theorem",
+    "conservation of mechanical energy"
+  ],
+  "num_results": 5
+}
+```
+
+### Use `/expand` for narrow technical queries
+
+Good candidates for expansion: named equations (Schrödinger, Navier-Stokes, Boltzmann), specific physical constants, or queries where the first search returns low-relevance results (distance > 0.4).
+
+### Interpret `distance` to judge relevance
+
+| Distance | Interpretation |
+|----------|---------------|
+| < 0.15   | Strong match — likely exactly what was asked for |
+| 0.15–0.30 | Good match — closely related concept |
+| 0.30–0.45 | Partial match — topically related but may not be the right theorem |
+| > 0.45   | Weak match — consider rephrasing or using `/expand` |
+
+### Show `informal_description` first, then `signature`
+
+For human-facing answers, lead with `informal_description` (natural language + LaTeX) and offer the formal `signature` as supporting detail. Most users want to understand the result before reading Lean 4 syntax.
+
+### Reconstruct the Lean import path from `name`
+
+The `name` array maps directly to the Lean import path:
+- `["Physlib", "Mechanics", "Newton", "secondLaw"]` → `Physlib.Mechanics.Newton.secondLaw`
+- Users can reference this in their Lean 4 files with `import Physlib.Mechanics.Newton`
+
+---
+
+## Rate limits
+
+| Endpoint | Limit |
+|----------|-------|
+| `/search` | 1 request/second |
+| `/fetch` | 10 requests/second |
+| `/expand` | 15 requests/minute |
+| `/modules` | 30 requests/minute |
+| `/modules/declarations` | 30 requests/minute |
+
+For agents making multiple searches in a loop, add a short delay between `/search` calls or batch queries into a single request (preferred).
+
+---
+
+## Declaration kinds
+
+Results can have these `kind` values:
+`theorem`, `definition`, `lemma`, `instance`, `axiom`, `structure`, `inductive`, `abbrev`, `opaque`, `example`, `proofWanted`, `classInductive`
+
+For most physics queries, `theorem` and `definition` are the most common and useful.
+
+---
+
+## More
+
+- **Live search**: https://physlibsearch.net
+- **API docs**: https://physlibsearch.net/docs
+- **Skill repo**: https://github.com/Kernel-Science/physlibsearch-skill
+- **Source**: https://github.com/Kernel-Science/physlibsearch
diff --git a/frontend/src/app/docs/page.tsx b/frontend/src/app/docs/page.tsx
@@ -84,6 +84,7 @@ export default function DocsPage() {
               ["overview", "Overview"],
               ["how-it-works", "How it works"],
               ["api", "API Reference"],
+              ["ai-agents", "AI Agents"],
               ["self-hosting", "Self-hosting"],
               ["open-source", "Open source"],
               ["next-steps", "Next steps"],
@@ -255,6 +256,50 @@ curl -s -X POST http://physlibsearch.net/search \\
             />
           </Section>
 
+          <Section id="ai-agents" title="AI Agents">
+            <p>
+              PhyslibSearch ships a{" "}
+              <a
+                href="https://claude.ai/code"
+                target="_blank"
+                rel="noopener noreferrer"
+                className="underline underline-offset-2 hover:text-foreground transition-colors"
+              >
+                Claude Code
+              </a>{" "}
+              skill that teaches any Claude agent how to call the API. Once installed, the agent can
+              search Physlib, fetch declarations by name, and expand queries with HyDE — without any
+              extra configuration.
+            </p>
+            <p className="text-foreground/50">Install the skill (one-time, any project):</p>
+            <CodeBlock
+              lang="bash"
+              code={`mkdir -p ~/.claude/skills/physlibsearch && curl -fsSo ~/.claude/skills/physlibsearch/SKILL.md \\
+  https://raw.githubusercontent.com/Kernel-Science/physlibsearch-skill/main/SKILL.md`}
+            />
+            <p>
+              Then invoke it in any Claude Code session with{" "}
+              <code className="font-mono text-xs bg-foreground/8 px-1 py-0.5 rounded">/physlibsearch</code>,
+              or just ask Claude to find a Lean theorem and it will load the skill automatically.
+            </p>
+            <p className="text-foreground/50">
+              To use it in a custom agent or system prompt, paste the raw{" "}
+              <code className="font-mono text-xs bg-foreground/8 px-1 py-0.5 rounded">SKILL.md</code>{" "}
+              content directly into your agent&apos;s context. The skill covers all endpoints,
+              example curl calls, query tips, and how to interpret the{" "}
+              <code className="font-mono text-xs bg-foreground/8 px-1 py-0.5 rounded">distance</code>{" "}
+              field.{" "}
+              <a
+                href="https://github.com/Kernel-Science/physlibsearch-skill"
+                target="_blank"
+                rel="noopener noreferrer"
+                className="underline underline-offset-2 hover:text-foreground transition-colors"
+              >
+                View on GitHub ↗
+              </a>
+            </p>
+          </Section>
+
           <Section id="self-hosting" title="Self-hosting">
             <p>PhyslibSearch runs on three services:</p>
             <ul className="list-disc list-inside flex flex-col gap-1 pl-2">
