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.
The article graph takes a different cut: nodes are Wikipedia articles, and there are two independent edge layers you can toggle. Shared-decl edges connect two articles that annotate the same Mathlib declarations — the result is a topical clustering, since articles that draw on the same parts of Mathlib pull together. A slider lets you raise the threshold for how many declarations two articles must share to be connected. Wikipedia link edges connect articles that link to each other through ordinary prose blue-links inside the cached enwiki HTML — the encyclopedia's own notion of related topics, independent of formalization. Nodes are colored by their dominant Mathlib namespace; only the shared-decl edges drive the force layout, so the Wikipedia-link layer is a true overlay.
The concept graph overlays two independent reference graphs on
the same Wikidata node set: 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) and Wikidata's typed item-to-item
statements (P279 subclass-of, P361 part-of, etc., pulled from the Wikidata Query
Service). Edges are colored by source so the consensus subgraph (where both systems
independently assert a relation) is visible at a glance.
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.