Mathlib: absorbing Wikipedia, Stacks, nLab, ProofWiki etc.

Stream: general

[Jeremy Lindsay]

Hi everyone,

I'd like to know if there have been any efforts made towards one of my fantasies—a community-generated mathematics wiki à la Wikipedia, Stacks, nLab, ProofWiki, etc. with the following features:

1. The wiki's frontend should be presented in $\LaTeX$, since the vast majority of mathematicians and students do not know Lean. Nevertheless, each and every theorem / definition should link to the mathlib docs. (This is also a marketing strategy for Lean.)
2. The wiki should acknowledge that mathematical terms are not univocal. For example, some textbooks do not require a ring to have a multiplicative identity. I'd like a wiki that makes clear precisely which mathlib definitions are used by various textbooks/papers. Mathematicians sometimes use subtly different definitions and assumptions; surely this is a source of errors. In future, mathematicians who are not yet interested in Leanifying their papers may nevertheless cite specific mathlib definitions for clarity.
3. The wiki should show the relationship between equivalent definitions; this is especially useful for definitions differing by 1, 2, or n assumptions. It could also be helpful for definitions that have changed over time, or that have been generalised.
4. The wiki should include (links to) completed Lean blueprints like PFR and the Liquid Tensor Experiment.
5. Within a proof, the wiki should contain mathlib links to every single definition, lemma, theorem, etc. referenced. No exceptions.

Some wilder fantasies:

6. The wiki should use a two-column proof style. The left column should show the proof itself (level-of-detail can be adjusted), automatically generated from the original Lean code but in a more readable format—this could be a $\LaTeX$-prettified version, a prosaic LLM-generated version (with options to change the language (English, Chinese, etc.)), a graphical representation, or even just the raw Lean code itself. In the right column, manual commentary can be added in the style of a paper or a textbook. This commentary could be sparse or detailed depending on need.
7. Every theorem or proof should make its required axioms clear. If the axiom of choice is used, for example, there might be a little yellow tag at the top labeled "AC".
8. The wiki should be automatically generated from mathlib like with doc-gen4 or leanblueprint, but without having to rely on docstrings for the $\LaTeX$. I have no idea how hard this is. Any additional prose accompanying the automatically generated $\LaTeX$ should be just that—additional, and manually entered like in the traditional encyclopaedias. I understand that this might go against the design philosophy of mathlib.
9. The wiki might even have support for different proof assistants, and links to their respective mathematics libraries. In that case, we would need a unified definition- and theorem-identifying system with unique IDs.

I've read about a few people trying to rewrite books in Lean, like Linear Algebra Done Right and Bourbaki, but I'm interested more in an eventual replacement for or addition to Wikipedia, Stacks, nLab, and ProofWiki.

I would love to get an idea of: what it would take to make a wiki like this, whether it exists already, whether it's even a good idea to begin with, how interesting it is to the Lean community, how interesting it would be to mathematicians at large, and whether or not it could be a good soft evangelism strategy for Lean.

Conclusion: blueprints are nice; why not expand them into a full-fledged encyclopaedia?

Thanks,
~ Jeremy

[Kevin Buzzard]

Feel free to run such a gigantic project! But it will take time and money.