Wikibrain API v3 — cells

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.

The model: cells, organs, supercells, synapses

The addressable thing is the cell — an atom of mathematics, id cell:<anchor>. A Mathlib declaration, a Wikidata concept, an external-database page, a WikiLean article and an arXiv statement that all denote one object are organs of that one cell: Module, Q18848 (module) and Q125977 (vector space) are the same atom, because Mathlib has no VectorSpace — Module generalizes it.

thing	what it is
organ	A particle — never a node. Kinds: `concept` (`Q<digits>`) · `decl` (`decl:<Lib>:<Name>`) · `page` (`xref:<db>:<id>`) · `article` (a WikiLean slug) · `statement` (`lit:<arxiv>#<ref>`). Payloads are EMBEDDED — the Lean code, the Wikidata description, the licensed DB snippet all ship on the cell.
cell	The atom, the node of the graph. `cell:<anchor>`, where the anchor is the cell's `exact` concept.
supercell	A Mathlib folder, `path:<Lib>/<Dir>`. Cells render inside it, and it owns organs of its own: field-of-study concepts (Q82571 "Linear algebra" → `path:Mathlib/LinearAlgebra`, not a cell) and area-level pages.
synapse	ONE aggregated edge per atom pair: `w` (weight — every constituent bond), a `kinds` histogram (`depends`, `links`, `relates`, `cites`, `mentions`, …) and the individual `traces`, each with its own direction, provenance and evidence. Undirected by construction, so there is no `dir` parameter.

Every v2 concept, declaration, container and article slug still resolves. aliases.json maps an organ id to its owning atom, and every route below accepts any such organ id or an atom id: Q125977, decl:Mathlib:Module and Vector_space all answer as cell:Q18848; Q82571 answers as path:Mathlib/LinearAlgebra.

Two v2 populations were dropped on purpose and 404 here (docs/BRAIN-V3.md "Dropped in v3") — the response names the reason rather than claiming the id is unknown: unanchored frontier ext pages (45,996 of 49,606 xref: ids — a page is an organ, and one no cell claims has no atom; the 3,610 anchored ones do resolve, the corpus stays in catalog/data/external/, and the page's signal survives as a co-page synapse) and arXiv paper nodes (1,994 lit:<arxiv> ids — only STATEMENTS a cell claims are organs). The cell layer is the only resolver.

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 nine tools: brain_bridge, brain_search, brain_cell, brain_transfer, brain_neighborhood, brain_snippets, brain_filter, decl_exists, brain_premises. brain_unit still answers, as an alias of brain_cell — the v2 unit card became the cell card. Rate limit: 120 requests/min per IP. Every response echoes snapshot:{generated_at,pin}.

Id grammar

form	what	example
`cell:<anchor>`	an atom (the node)	`cell:Q18848`
`path:<Lib>[/<Dir>…]`	supercell (Mathlib folder)	`path:Mathlib/LinearAlgebra`
`Q<digits>`	concept organ (Wikidata QID)	`Q181296`
`decl:<Lib>:<FQ name>`	decl organ	`decl:Mathlib:CommGroup`
`xref:<db>:<id>`	page organ (external DB)	`xref:nlab:module`
`lit:<arxiv>#<ref>`	statement organ	`lit:1707.04448#thm1.2`

REST endpoints

GET /api/brain/cell?key=

Resolve any organ id — QID, decl:Lib:Name, bare decl name, article slug, xref:db:id, lit:…, an exact label or aka, or an atom id — to the owning atom's card: the cell head, every organ with its embedded payload, the containment breadcrumb, a synapse summary and the strongest partners. One request renders the whole card. /api/brain/unit?key= is an alias (the v2 unit card became the cell card).

curl 'https://wikilean.jackmccarthy.org/api/brain/cell?key=CommGroup'
curl 'https://wikilean.jackmccarthy.org/api/brain/cell?key=Vector_space'   # → cell:Q18848

GET /api/brain/transfer?q=&direction=&limit=

The informal ↔ formal jump. direction=informal_to_formal: concept text / QID / slug → the atom's ranked Mathlib decl organs with modules, docs URLs and bond. direction=formal_to_informal: a decl name → the same atom's concept organs, article URLs and snippet sources. A field-of-study concept answers with its supercell (folder), which is the honest formal home. 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=Module&direction=formal_to_informal'

GET /api/brain/bridge?q=&limit=

The composite first call of an autoformalization loop: an informal statement in, existence-verified Mathlib decls out — each with its code signature, module + import_line, bond quality (exact vs generalization/…), the atom's breadcrumb, and capped one-hop depends synapses. Abstains honestly: below the confidence floor it returns match:"none" with the nearest atoms instead of a forced answer, and says so in match_rule. Ends with next_tools hints.

curl 'https://wikilean.jackmccarthy.org/api/brain/bridge?q=every%20finitely%20generated%20vector%20space%20has%20a%20basis'

GET /api/brain/decl?name= | names=<csv, ≤16>

Existence oracle for declaration names — batch it: agents draft statements citing several decls, and one round-trip beats eight. Per name: exists, and when false, namespace resolution over the FULL decl index: a renamed_to suggestion labelled by suggestion_basis — "verified-rename" (an agent read the declaration in the checkout and an adversarial verifier upheld it) vs "namespace-resolution" (exactly one indexed decl shares the final segment, oracle-verified — a lead, not a fact). When 2–8 decls share the segment the verified list returns as namespace_matches:[{decl,module}] with no forced pick; more than 8 returns namespace_match_count + a hint to qualify the namespace.

curl 'https://wikilean.jackmccarthy.org/api/brain/decl?names=Basis,Module.Basis,AddCircle.fourierCoeff,NotARealName'

GET /api/brain/premises?seeds=<csv, ≤8>&limit=

Stored-premise retrieval for proof drafting — use it after search, never instead of it: seed with the anchor theorems you already found (1–8 fully-qualified decl names) and get back the ranked union of the premises their stored proofs actually used. Ranking = multiplicity across seeds, then stored per-seed rank; every row is oracle-verified and carries module + import_line + score + via (the seeds that cite it). A dead seed that namespace-resolves uniquely is auto-resolved and says so (resolved_via in seeds_resolved); unresolvable seeds return in seeds_unknown instead of failing the call. limit defaults 20, cap 50.

curl 'https://wikilean.jackmccarthy.org/api/brain/premises?seeds=Nat.ModEq.pow_totient,Nat.totient_prime'

GET /api/brain/neighborhood?id=&kinds=&limit=&traces=&min_w=&min_conf=&cursor=

An atom's synapses: one row per partner atom with w, the kinds histogram, traces_total, and the traces themselves (each {kind, src, dst, prov, evidence} — src/dst are the ORGAN ids that witnessed the bond). kinds is a CSV subset of the 11 synapse kinds — depends,links,mentions,cites,relates,co-page,co-statement,invocation,related,special_case,generalization; limit ≤ 200; traces=0 omits traces for a compact partner list. No dir: a synapse is an undirected aggregate — direction lives on each trace. formalizes/matches are not synapse kinds: the merge function consumes them as organ attachments, so read them off an organ's bond on /api/brain/cell. A supercell's rows are hydrated from the partner cells' shards (traces_hydrated); where a trace is unreachable the row says so in traces_unavailable instead of shipping an empty list.

curl 'https://wikilean.jackmccarthy.org/api/brain/neighborhood?id=Q18848&kinds=depends'

GET /api/brain/snippets?id=

Every stored content snippet on an atom, read from the embedded organ payloads (no fan-out): Wikidata description (CC0), WikiLean article pointer, each page organ's stored snippet, the Mathlib docstring + code, and arXiv statement links. Every row carries its license; no-content sources (MathWorld, DLMF, EoM, Kerodon) return deep links only, and arXiv statement text is never redistributed.

curl 'https://wikilean.jackmccarthy.org/api/brain/snippets?id=Q181296'

GET /api/brain/filter?f=&type=&under=&limit=&cursor=

Enumerate atoms whose facet bitmask contains f (i.e. (f_row & f) == f). type=cell (default) reads each cell's OWN mask; type=supercell reads fa, the subtree-AGGREGATE mask. under=path:… restricts to a containment subtree. Bits (brain/SCHEMA.md): 0 gold @[wikidata] · 1 @[stacks] · 2 @[kerodon] · 3 any xref · 4 formalized · 5 partial · 6 has WikiLean article · 7 has literature · ~~8 is ext~~ (never set on a cell — external pages are organs) · 9 lmfdb · 10 nlab · 11 mathworld · 12 proofwiki · 13 stacks-tag · 14 oeis · 15 has stored snippet. Paginate with the returned next_cursor.

curl 'https://wikilean.jackmccarthy.org/api/brain/filter?f=1&limit=50'
curl 'https://wikilean.jackmccarthy.org/api/brain/filter?f=1&under=path:Mathlib/Algebra'

GET /api/brain/search?q=&type=&limit=

Label search over the atom index. Matches an atom's own label AND its aka list — every organ's label — so q=Vector space returns the Module atom. A key that resolves exactly (QID, decl name, slug, xref id) is promoted to the top hit. type ∈ cell|supercell.

curl 'https://wikilean.jackmccarthy.org/api/brain/search?q=vector%20space'

Related routes

GET /api/brain/edges?id= (live community overlay, uncached) · GET /decl/<name> (decl → docs redirect; JSON with Accept: application/json).

Provenance & licensing

Brain cell/synapse data is CC0. Every organ and every synapse trace carries a prov index into the shard manifest's prov table. 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 · Mathlib Apache-2.0); other sources deep-link out.