Connect mathematical writing to formal proofs. WikiLean links passages in Wikipedia’s mathematics articles to Lean declarations, with evidence readers can inspect and improve.
Browse articles · Contribute · Explore the Brain
- Check a match: open an article, select a passage, and confirm or report its link.
- Add or correct a tag: sign in, accept the CC0 agreement, and save a declaration with its relation to the passage. Tags are public and attributed.
- Use your own agent: create an account for it at /agents. Keep your model credentials and spending limits on your own machine.
- Work on the pipeline or Brain: follow the contributor guide. Submit sealed pipeline results using the self-service intake client. Validation produces a receipt; publication remains a separate step.
Matches are preliminary. Lean verifies formal proofs, but the match between a formal statement and a passage still needs review. An unsuccessful search covers only the libraries and versions searched.
| Area | Purpose | Start here |
|---|---|---|
wiki/ |
Live Worker, reader, accounts, community tags | Worker guide |
scripts/articles/ |
Formalization reader builds and contribution intake | Articles, intake |
brain/ |
Concept, code, database, and literature graph | Brain API, schema |
site/, catalog/ |
Annotation, moderation, upstream data, asset sources | Catalog |
bot/ |
Human-reviewed @[wikidata] contributions to Mathlib |
Bot sources |
manage/ |
Coverage and worklists | Management |
For development commands and the contribution policy, read CONTRIBUTING.md. For project direction, read the canonical roadmap. HANDOFF.md is the operator and agent entry point.
D1 is canonical for article annotations, revisions, and community edits. Files in
site/annotations/ are caches and backups, never a replacement for live edits.
The formalization reader uses a published record-set store plus community tags
from D1. The Brain serves immutable, verified releases with a community overlay.
Canonical annotations use Literature Links. The native conversion and contributor release are documented in the November 8 activation record. Historical activation records describe past deployments; check the live /api/version for current identity.
All production changes follow the release runbook. CI validates changes; it does not deploy them.
Code is MIT; WikiLean annotation data is CC0. Wikipedia text remains CC BY-SA, and Lean code retains its library’s licence. Read the data and research notice before contributing.