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.