Skip to content

SKILL.md

Latest commit

 

History

History
249 lines (185 loc) · 7.96 KB

SKILL.md

File metadata and controls

249 lines (185 loc) · 7.96 KB
Raw
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

{
  "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)

[[
  {
    "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)

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)

"Schrödinger equation for a free particle"

Response — JSON string (expanded query or original on failure)

"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

# 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

{
  "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)

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

[
  {"name": ["Physlib", "Mechanics"], "count": 42},
  {"name": ["Physlib", "QuantumMechanics"], "count": 31}
]

Example (curl)

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)

["Physlib", "Mechanics", "Newton"]

Response — list[Record] (same shape as search results, without distance)

Example (curl)

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:

{
  "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