paper about mathlib

Stream: general

[Rob Lewis]

A group of us are trying to write up a paper that describes the design and organization of mathlib. There are around 65 contributors to mathlib so far. Rather than attributing the paper to some subset as authors, we thought we'd submit it as a community effort. All contributors will be acknowledged, and none will be official authors. As well as a (hopefully) nice paper, this should be good high-level documentation about the library.

What this means: as community members, you can help us write the paper :) there are a few things we'd like to include that anyone could tackle. One is documentation, e.g. https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/linear.20algebra.20documentation.20push . It can be tough to document something you didn't write yourself, but if you're partially familiar with some of it, this could be a good way to learn more.

Something else we'd like are pictures. It would be great to include e.g. graphs of the import structure, (parts of) the type class hierarchy, etc. @Patrick Massot has a script here that's a great start for graphing the import structure, but it needs some small fixes and some attention to format a pretty graph.

Please let us know if you're willing to help out with some of this!

[Rob Lewis]

Patrick generated imports.graphml , a graph of the import structure, which can be edited at https://www.yworks.com/yed-live/ (or with the yEd software). The challenge is to optimize it for display in a paper. Reading labels is out of the question, but hopefully there's a nice way to color and/or group things. We can also host a huge legible version elsewhere.

[Sebastian Ullrich]

(Are there any advantages of this format/program over dot? I may want to build similar graphs very soon)

[Patrick Massot]

The advantage is there is some software which does both automatic layout and manual tweaking.

[Patrick Massot]

Graphviz is only automatic, and Dia is only manual.

[Patrick Massot]

I should add that the graph was generated by https://leanprover.zulipchat.com/user_uploads/3121/jDimxYPQI7nz7JYjAh1mVm1y/import_graph.py which is very easy to tweak, especially adding meta-data to nodes if anyone finds a way to make something with them. Of course this forces me to reveal that no Lean meta-programming was involved in creating this graph...

[Sebastian Ullrich]

I fear I would have chosen the same language anyway

[Sebastian Ullrich]

I didn't even think of manually layouting such humongous graphs, but if it's a part to be published that could be an advantage I suppose

[Patrick Massot]

Originaly I wrote that python script for a smaller project where the graph is manageable, after an initial automatic layout.

[Rob Lewis]

A group of us are trying to write up a paper that describes the design and organization of mathlib. There are around 65 contributors to mathlib so far. Rather than attributing the paper to some subset as authors, we thought we'd submit it as a community effort. All contributors will be acknowledged, and none will be official authors. As well as a (hopefully) nice paper, this should be good high-level documentation about the library.

We've finished a draft of this paper. Comments and suggestions are very welcome! https://leanprover-community.github.io/papers/mathlib-paper.pdf

This is a "semi-public" draft. Please don't spread it too far, e.g. on Twitter.

[Rob Lewis]

The draft has been updated and is now public: https://leanprover-community.github.io/papers/mathlib-paper.pdf

Thanks to everyone who helped write and commented on it!

[Rob Lewis]

The community paper is accepted at CPP. Congrats, coauthors!