| 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
EXPANDED=$(curl -s -X POST https://physlibsearch.net/expand \
-H "Content-Type: application/json" \
-d '"Schrödinger equation for a free particle"')
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
