Wikibrain API v2
Read-only, unauthenticated, cached (Cache-Control: public, max-age=3600 —
data rebuilds nightly). Base URL https://wikilean.jackmccarthy.org.
Full reference with response schemas: docs/BRAIN-API.md.
Connect over MCP (recommended for agents)
claude mcp add --transport http wikibrain https://wikilean.jackmccarthy.org/mcp
A dependency-free streamable-HTTP MCP server (JSON-RPC 2.0, stateless, single-response
mode) exposing eight tools: brain_search, brain_node,
brain_unit, brain_transfer, brain_neighborhood,
brain_snippets, brain_filter, decl_exists.
Rate limit: 120 requests/min per IP.
Node id grammar
| form | type | example |
|---|---|---|
Q<digits> | concept (Wikidata QID) | Q181296 |
path:<Lib>[/<Dir>…] | container (Mathlib folder) | path:Mathlib/CategoryTheory |
decl:<Lib>:<FQ name> | Lean declaration | decl:Mathlib:CommGroup |
lit:<arxiv>#<ref> | literature statement | lit:1707.04448#thm1.2 |
xref:<db>:<id> | external DB page | xref:lmfdb_knowl:group.abelian |
REST endpoints
GET /api/brain/unit?key=
Resolve any member key — QID, decl:Lib:Name, bare decl name,
article slug, xref:db:id, or exact concept label — to the owning concept's
atomic unit card (article ∘ QID ∘ decls ∘ containers ∘ cross-refs).
curl 'https://wikilean.jackmccarthy.org/api/brain/unit?key=CommGroup'
GET /api/brain/transfer?q=&direction=&limit=
The informal ↔ formal jump. direction=informal_to_formal: concept text /
QID / slug → ranked Mathlib decls with modules, docs URLs, match_kind and
confidence. direction=formal_to_informal: a decl name → concepts, article
URLs and snippet sources. Empty results include near-miss suggestions.
curl 'https://wikilean.jackmccarthy.org/api/brain/transfer?q=abelian%20group&direction=informal_to_formal'
curl 'https://wikilean.jackmccarthy.org/api/brain/transfer?q=CommGroup&direction=formal_to_informal'
GET /api/brain/neighborhood?id=&kinds=&dir=&limit=
Filtered projection of a node's typed edges. kinds is a CSV of
formalizes,mentions,depends,matches,xref,relates,links,cites;
dir ∈ out|in|both; limit ≤ 200.
curl 'https://wikilean.jackmccarthy.org/api/brain/neighborhood?id=Q181296&kinds=xref&dir=out'
GET /api/brain/snippets?id=
Every stored content snippet for a unit — Wikidata description, WikiLean article pointer, and each cross-referenced external page's stored snippet — with a per-row license. No-content sources (MathWorld, DLMF, EoM, Kerodon) return deep links only.
curl 'https://wikilean.jackmccarthy.org/api/brain/snippets?id=Q181296'
GET /api/brain/filter?f=&type=&limit=&cursor=
Enumerate nodes whose facet bitmask contains f (i.e. (node.f & f) == f).
Bits (brain/SCHEMA.md): 0 gold @[wikidata] · 1 @[stacks] ·
2 @[kerodon] · 3 any xref · 4 formalized · 5 partial · 6 has article ·
7 has literature · 8 is ext · 9 lmfdb · 10 nlab · 11 mathworld · 12 proofwiki ·
13 stacks-tag · 14 oeis · 15 has snippet. Bits 0–2 sit on the tagged decl AND
propagate to the concept(s) it formalizes. Paginate with the returned
next_cursor.
curl 'https://wikilean.jackmccarthy.org/api/brain/filter?f=1&limit=50'
Existing routes
GET /api/brain/node?id= (full shard entry) ·
GET /api/brain/search?q=&type=&limit= (label search) ·
GET /api/brain/edges?id= (live community overlay, uncached) ·
GET /decl/<name> (decl → docs redirect; JSON with Accept: application/json).
Provenance & licensing
Brain node/edge data is CC0. Every edge carries provenance
(prov_table on /api/brain/node). Snippets are stored only where
the source license permits and each row carries its license
(nLab attribution · Stacks GFDL · LMFDB/OEIS CC-BY-SA-4.0 · ProofWiki CC-BY-SA-3.0 ·
PlanetMath CC-BY-SA); other sources deep-link out.