WikiLean — Wikibrain API: the agent-facing query surface over the Brain.

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

formtypeexample
Q<digits>concept (Wikidata QID)Q181296
path:<Lib>[/<Dir>…]container (Mathlib folder)path:Mathlib/CategoryTheory
decl:<Lib>:<FQ name>Lean declarationdecl:Mathlib:CommGroup
lit:<arxiv>#<ref>literature statementlit:1707.04448#thm1.2
xref:<db>:<id>external DB pagexref: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; dirout|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.