WikiLean is a mirror of WikiProject Mathematics articles, annotated inline with links into Mathlib4 and color-coded by whether each definition, theorem, and proof has been formalized in the Lean proof assistant.
Three stages. Catalog: enumerate the WikiProject Mathematics article set with its metadata and Wikidata identifiers. Annotate: for each article, work through its definitions, theorems, and proofs and match each one to the Mathlib4 declaration that formalizes it, recording a status and the declaration's module path. Host: fetch the article's rendered HTML from the MediaWiki API, wrap each matched statement in place, and serve the result as a standalone page. Hovering (or tapping) a highlighted statement shows its status and a direct link into the Mathlib documentation.
Each article is annotated against a specific Wikipedia revision, and that revision id is recorded alongside the annotations, so a highlight always refers to the exact prose it was made against even after the live article changes. Mathlib links point at the public Mathlib4 documentation.
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.
For AI agents, the same graph is queryable as the Wikibrain MCP server and the Wikibrain REST API: resolve any informal concept to its exact Mathlib declaration (with match quality and docs link), or start from a Lean name and pull the surrounding informal context — the article, the Wikidata identity, and every cross-referenced external database. Each answer carries provenance and confidence.
The Brain is a zoomable map over one shared node set: a
containment bubble view (libraries → areas → concepts, nesting by generality)
and a dependency web/ego view overlaying independent reference graphs —
Mathlib's declaration-level dependency edges (extracted via Expr.getUsedConstants
over the built Mathlib environment — the same data that produces hyperlinks in the
Mathlib docs), Wikidata's typed item-to-item statements (P279 subclass-of, P361
part-of, etc.), cross-database identities, and the literature. Every edge carries its
provenance — human / machine / AI — which is filterable, and a sources view
documents where every external link comes from, with its Wikidata property and license.
Annotations are best-effort and cover a growing 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 are welcome via the source repository.