A REST + GraphQL API over every verified theorem, its proof, lineage, and downstream uses. Free for individual academics, metered for labs and enterprise.
Pass your API key as a Bearer token. Generate keys from your API keys page. Never embed keys client-side.
curl https://api.nasrudin.dev/v1/theorems/9f3a2c8e \ -H "Authorization: Bearer nsk_live_a98c…"
Returns the full theorem record: statement (Lean & MathML), proof, provenance, lineage IDs, and downstream theorem IDs.
curl https://api.nasrudin.dev/v1/theorems/9f3a2c8e \ -H "Authorization: Bearer $NSR_KEY"
Full-text + structural search across statements, names, and Lean tactics.
curl "https://api.nasrudin.dev/v1/search?q=commutator&domain=quantum&limit=20" \ -H "Authorization: Bearer $NSR_KEY"
Server-sent events. Subscribe with optional domain filters and receive each newly verified theorem within ~2s of server acceptance.
const es = new EventSource("https://api.nasrudin.dev/v1/stream?domain=quantum"); es.onmessage = (e) => console.log(JSON.parse(e.data));
| Tier | Reads / day | Stream |
|---|---|---|
| Free | 10,000 | — |
| Researcher | 10,000 / day | ✓ |
| Lab | 250,000 / day | ✓ |
| Enterprise | custom | ✓ |