diff --git a/AGENTS.md b/AGENTS.md
index 0714ca55c..6e1665c52 100644
--- a/AGENTS.md
+++ b/AGENTS.md
@@ -95,7 +95,7 @@ brain/acquire-wikidata-entities.sh /absolute/private/request-plan.json \
them `ai-moderated` — **AI-changed bytes are never left marked `human`, and bots never
mint `human`** (endorse stays session-only; 403). Humans gate only cross-site pushes.
- **Render-cache keys are manually versioned + load-bearing** (currently `render:v17:`,
- `page:home:v10`, `page:articles:v2`, `page:articles-index:v1`, `page:about:v1`,
+ `page:home:v10`, `page:articles:v3`, `page:articles-index:v1`, `page:about:v2`,
`page:sitemap:v4`, `page:stats:v5`, `page:wikifunctions:v3`,
`page:wikifunctions-verify:v3` — all in `index.ts`) — bump the
prefix whenever output bytes change, or readers get stale HTML for up to 30 days. Asset
diff --git a/CLAUDE.md b/CLAUDE.md
index b42de245d..6f93d0efa 100644
--- a/CLAUDE.md
+++ b/CLAUDE.md
@@ -95,7 +95,7 @@ brain/acquire-wikidata-entities.sh /absolute/private/request-plan.json \
them `ai-moderated` — **AI-changed bytes are never left marked `human`, and bots never
mint `human`** (endorse stays session-only; 403). Humans gate only cross-site pushes.
- **Render-cache keys are manually versioned + load-bearing** (currently `render:v17:`,
- `page:home:v10`, `page:articles:v2`, `page:articles-index:v1`, `page:about:v1`,
+ `page:home:v10`, `page:articles:v3`, `page:articles-index:v1`, `page:about:v2`,
`page:sitemap:v4`, `page:stats:v5`, `page:wikifunctions:v3`,
`page:wikifunctions-verify:v3` — all in `index.ts`) — bump the
prefix whenever output bytes change, or readers get stale HTML for up to 30 days. Asset
diff --git a/wiki/src/home.ts b/wiki/src/home.ts
index 56c6fc9ed..60ead64e3 100644
--- a/wiki/src/home.ts
+++ b/wiki/src/home.ts
@@ -2,8 +2,8 @@
// Replaces the static site/out/ pages that build-public.ts used to copy into
// wiki/public/ — articles created via PUT /api/article/:slug now appear
// without a static rebuild. index.ts serves brainLanding() cached in
-// RENDER_CACHE ('page:home:v10', TTL 300s), homePage() ('page:articles:v2',
-// TTL 300s), aboutPage() ('page:about:v1', TTL 300s), and sitemapXml()
+// RENDER_CACHE ('page:home:v10', TTL 300s), homePage() ('page:articles:v3',
+// TTL 300s), aboutPage() ('page:about:v2', TTL 300s), and sitemapXml()
// ('page:sitemap:v4', TTL 3600s).
//
// Visual language: warm academic-minimalist — paper background, serif display
@@ -471,8 +471,8 @@ footer a:hover { text-decoration:underline; }
cross-database pages, and literature — with machine-checkable
provenance on every edge.
Wikidata concept links — every formalized concept keyed
- to its Wikidata item, as an open RDF dataset (the basis for a proposed
- “formalized as (Lean/Mathlib)” Wikidata property).
+ to its Wikidata item, as an open RDF dataset (Wikidata’s property for these
+ links is “Mathlib Declaration ID”, P14534).
Wikibrain MCP — a remote MCP server any AI agent can
connect to mid-proof: jump between informal mathematics and formal
Mathlib declarations (full REST reference at /brain/api).
@@ -565,7 +565,7 @@ export interface AboutStats {
nNotFormalized: number;
}
-// The About & method page, served dynamically from D1 (KV 'page:about:v1',
+// The About & method page, served dynamically from D1 (KV 'page:about:v2',
// TTL 300s). Replaces the static site/out/about.html asset (retired from
// build_static_pages.py) whose baked stats went stale the day it was built.
// Visual shell reproduced from that page: self-contained inline CSS, warm
@@ -695,10 +695,10 @@ footer p { margin:4px 0; }
Wikidata concept links
Every concept matched to a formalized declaration is also keyed to its
Wikidata item and published as an open
- RDF dataset. This is the basis for a proposed Wikidata
- property, “formalized as (Lean/Mathlib)” — the long-term goal is
- for these links to live in Wikidata itself, maintainable by the community and queryable
- via SPARQL.
+ RDF dataset. Wikidata has a property for these links,
+ “Mathlib Declaration
+ ID” (P14534); the long-term goal is for them to live in Wikidata
+ itself, maintainable by the community and queryable via SPARQL.
For AI agents: the Wikibrain MCP
For AI agents, the same graph is queryable as the
@@ -720,14 +720,36 @@ footer p { margin:4px 0; }
documents where every external link comes from, with its Wikidata property and license.
Limitations & how to contribute
-
Annotations are best-effort and cover a growing sample of WikiProject Mathematics,
+
Annotations are best-effort and cover a sample of WikiProject Mathematics,
not the whole corpus. A match reflects a judgment that a Mathlib declaration formalizes
a statement; it can be incomplete or wrong, and Mathlib itself evolves, so coverage is
- a snapshot rather than a guarantee. Corrections happen right on the site: sign in
- (GitHub or Google) to edit annotations in-context on any article, or — without an account — report
- a problem from any annotation's tooltip (the ⚑ link). Human edits are patrolled by
- moderators, and AI proposals to change a human-authored annotation are queued for
- human approval before anything lands.
+ a snapshot rather than a guarantee. Corrections happen right on the site:
+ sign in to edit annotations in-context on any article, or — without
+ an account — report a problem from any annotation's tooltip (the ⚑ link).
+
+
How edits are moderated
+
Annotation edits by people take effect immediately and are shown as human-curated.
+ They are not screened first: each one is listed, newest first, in
+ Recent changes with an awaiting-patrol marker,
+ and the Stats page shows how many have been patrolled. Every change
+ to an article’s annotations, by a person or by the AI pipeline, is recorded in the
+ article’s history, and patrollers can restore an article’s annotations to
+ any earlier version in that history.
+
The AI pipeline cannot silently overwrite a human-curated annotation: a pipeline save
+ that drops or alters one is refused, and the pipeline can file a proposal instead. Under
+ WikiLean’s human-at-boundaries policy (adopted August 2026), those proposals no
+ longer need a person’s approval. Each night a deterministic resolver, which uses no
+ language model, approves or rejects the proposals that match its fixed rules; the rest
+ stay pending until a patroller or a later nightly run decides them, or lapse when the
+ pipeline next saves the article and finds their target annotation removed or already
+ matching them. When the pipeline approves a change to a human-curated annotation, the
+ annotation is relabeled: it is then shown as “AI-generated · not yet
+ reviewed” and loses the human-curated protection, so later pipeline saves can
+ change it directly. When a patroller approves a change, the result is shown as
+ human-curated. People remain the gate wherever WikiLean contributes
+ to outside projects: the tagging bot opens pull requests to Mathlib on its own, but they
+ merge only after Mathlib reviewers approve them, and statements are added to Wikidata
+ only for mappings people have reviewed.