The scientific process produces different kinds of knowledge, obtained over different spans of time. Research focused on “implementing mathematics,” specifically capturing definitions, theorems, and proofs, requires a solid understanding of the foundations of mathematics and its encoding using computers. Issues of usability come next, where overly pure approaches to foundations become humanly infeasible to work with.

However, a rather different sort of knowledge emerges when looking at implementing mathematics at a scale involving a large library, a lot of people, over a long period of time. Scaling issues have a tendency of becoming folk knowledge within a small community, and then becoming lost over time.

Which brings us to the paper at hand: it brilliantly captures a plethora of “folk knowledge,” of immense value to current and future system builders (and historians and social scientists and so on). Via a chronological walk-through of the development of the Mizar system, the authors present a series of lessons learned. These are carefully put into the appropriate context, be it temporal, cultural, geopolitical, or mathematical. This is augmented by a wealth of nicely chosen statistics that help illustrate the full breadth of the issues involved in building the Mizar Mathematical Library.

The authors take great pains to emphasize that the true value of a system (such as Mizar) really lies in the ecosystem built around its library, the real repository of knowledge, rather than in the base software. As true mathematicians, they make their case primarily through data, although a few well-chosen opinions from other scientists are added for good measure.

Anyone with an interest in building systems for mathematics should read this paper. They will get a preview of the kinds of forces at play when a small team succeeds in pushing a system forward, through decades of hard work, to create a large, well-structured system that is still used today. Hopefully, the reader will be struck, as I was, with the breadth and thoroughness of the issues covered in their tale. This paper is not just enlightening; it is also fun to read.