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.
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.