Licensing the Mizar Mathematical Library

TL;DR

This paper discusses the process and decisions involved in establishing a clear licensing policy for the Mizar Mathematical Library, a large formalised mathematical knowledge base, to clarify legal status and ensure long-term sustainability.

Contribution

It presents the specific copyright and license solutions adopted for Mizar, providing insights and experience for similar formal mathematical libraries.

Findings

Legal clarification of MML's status achieved

A tailored licensing policy established for Mizar

Guidance for other formal library communities provided

Abstract

The Mizar Mathematical Library (MML) is a large corpus of formalised mathematical knowledge. It has been constructed over the course of many years by a large number of authors and maintainers. Yet the legal status of these efforts of the Mizar community has never been clarified. In 2010, after many years of loose deliberations, the community decided to investigate the issue of licensing the content of the MML, thereby clarifying and crystallizing the status of the texts, the text's authors, and the library's long-term maintainers. The community has settled on a copyright and license policy that suits the peculiar features of Mizar and its community. In this paper we discuss the copyright and license solutions. We offer our experience in the hopes that the communities of other libraries of formalised mathematical knowledge might take up the legal and scientific problems that we addressed for Mizar.