WikiLean

Live at wikilean.jackmccarthy.org — an annotated mirror of Wikipedia's mathematics articles, with each definition, proposition, theorem, and example mapped (where possible) to its formalization in Mathlib4, the Lean 4 mathematics library.

A reader can scan an article and see at a glance which statements are formalized (green), partially formalized (yellow), or not yet formalized (red), with a one-click link out to the Mathlib declaration. A formalizer can use the same view as a coverage map: "what's a notable concept Mathlib hasn't reached yet?"

Current status (October 2026)

• The editable wiki is live. Sign in with GitHub to add, correct, or discuss annotations directly in an article. D1 remains the canonical store for article annotations, revisions, moderation state, and the community-edge overlay.
• The immutable Brain release has been live in production since 2026-10-04. /assets/brain/current.json selects release sha256:8305822b… (manifest fa645b2b…), a brain-offline-replay-v1 build from authority commit 2eb31baa (PR #43). The promoter's canary failed that day because Cloudflare Web Analytics adds bytes to text/html responses (fixed in PR #44). The attempt was reconciled on 2026-10-08 (journal outcome deployed_reconciled), so no incomplete attempt blocks the next promotion. See the activation record. The repository has no automatic deploy-on-merge workflow.
• Live annotation snapshot checked on 2026-10-13: 778 articles and 37,936 annotated statements: 27.9% formalized and 14.1% partial. Current numbers are on /about and /stats.
• Two complementary editable exports remain keyed to Wikidata entities: the per-article W3C annotation layer (generated locally by site/export_w3c.py into the gitignored site/out_w3c/; not published) and the per-QID RDF concept layer. The site separately serves an annotation-derived RDF dump at /wikilean.ttl, generated by site/export_wikidata_rdf.py.
• Upstream work: Wikidata property P14534 (Mathlib Declaration ID) was created on 2026-06-17 from the property proposal; Mathlib @[wikidata] tags provide the other direction of the same mapping.

Architecture

WikiLean has two deliberately separate data planes:

1. Mutable collaboration plane. The Cloudflare Worker in wiki/ serves articles, authentication, review tools, REST endpoints, and MCP. D1 is canonical for article annotations and revisions; KV holds caches. Seeding is edit-safe and never overwrites an article with a real user revision.
2. Immutable Brain plane. The Brain is a graph of mathematical cells. A cell combines organs that denote the same mathematical object: Wikidata concepts, Mathlib declarations, WikiLean articles, external-database pages, and literature statements. Mathlib folders are supercells; provenance-bearing relationships between cells are aggregated as synapses. brain/SCHEMA.md is the normative data contract.

The target immutable release path implemented by the merged tooling is:

reviewed sources + explicit sealed acquisitions
                       |
                       v
 source plan + receipts + normalization lineage
                       |
                       v
       deterministic, network-free replay
                       |
          +------------+-------------+
          |                          |
          v                          v
 reviewable JSONL graph       SQLite query projection
          |
          v
 cells + synapses + shards + release-neutral /brain page
          |
          v
 frozen release: logical release_id + exact manifest_sha256
          |
          v
 reviewed public baseline + activation evidence bundle
          |
          v
 explicit operator promotion to the Cloudflare Worker
          |
          +--> /brain and immutable release assets
          +--> /api/brain/*
          +--> POST /mcp

Acquisition is separate from replay. Networked tools first capture immutable source objects and evidence; the reducer then runs offline from an explicit inventory. JSONL is the reviewable source of truth, while SQLite is a generated local query projection and is never a Cloudflare asset. Production has served a full offline replay release since 2026-10-04, but the nightly still freezes the compatibility profile; nothing on main automates the next replay release.

Every frozen release has two identities. release_id names the logical graph content; manifest_sha256 names the exact release.json bytes and therefore the public namespace /assets/brain/releases/<manifest_sha256>/. A v2 selector at /assets/brain/current.json chooses the current and optional previous manifest. The Worker resolves that selector once per request, verifies the exact manifest, and verifies every manifest-declared JSON asset before parsing it. The browser follows the same rule.

The nightly may acquire approved inputs, build, test, freeze, and shadow-stage a candidate, but it cannot deploy. Production promotion requires a reviewed public baseline, a reviewed activation bundle, an unchanged clean main, exact toolchain identities, a durable journal, and a release-qualified canary. See the Brain API, authority contracts, and release runbook.

Release state is four separate facts

State	Current value
Architecture code merged to main	Yes
New Worker/site bundle deployed	Yes: promoted 2026-10-04 from authority commit 2eb31baa. main has changed wiki/src since (for example #46, #47, #54 and #63); those changes reach production only with the next release
Immutable Brain release assets published	Yes: release sha256:8305822b…, manifest fa645b2b…
Production selector activated	Yes: v2 selector, audited_at 2026-10-04T17:25:04Z, no previous release

Checked on 2026-10-13; see the activation record. A successful merge or CI run changes only the first row. It does not deploy Worker code, publish Brain data, or authorize activation.

Repository layout

Path	What's there
catalog/ — see catalog/README.md	Catalog of WikiProject Math articles, AI Mathlib-tagging, concept layer, RDF export, Wikidata enrichment.
site/	Annotation pipeline (render.py, batch_annotate.py), local review editor (serve_review.py), W3C export, sources for the static fallback.
wiki/ — see wiki/README.md	Cloudflare Worker + D1 backend that serves the live editable site.
brain/	Brain schema, deterministic reducer, acquisition and replay contracts, SQLite projection, release builder, and verification tests.
site/ops/	Shadow nightly, public-baseline freezer, activation evidence, promotion journal, exact release promoter, and canary.
bot/	Human-gated automation for upstream Mathlib @[wikidata] work.
manage/	Coverage and centrality control plane for choosing the next work.
wikifunctions/	QID → Wikifunctions ZID → Mathlib data pipeline behind /wikifunctions; the verification project moved to Deicyde/wikifunctions.
docs/	Long-form docs (Wikidata property proposal, …).

How to contribute

Three independent paths, you can pick any:

1. Annotate articles directly on the live site. Sign in with GitHub at wikilean.jackmccarthy.org, open any article, hover a highlight to edit it, or select text to add a new one. Edits are saved to D1 and visible to the next reader. See CONTRIBUTING.md.
2. Improve the pipeline / engine. Patches to site/, wiki/, or catalog/ welcome. See CONTRIBUTING.md.
3. Help upstream. Add or check P14534 (Mathlib Declaration ID) statements on Wikidata concept items, or review the in-flight Mathlib @[wikidata] PRs (see the docs).

License

Code: MIT. Annotation data is published under CC0 (it's a description of Wikipedia + Mathlib, both public). Article text shown on the site remains under the original CC BY-SA terms of the upstream Wikipedia source.

If you contribute, please also read the data & research notice and the token-donation policy in CONTRIBUTING.md — they cover how edit metadata may be studied and how donating compute will work.