Pith. sign in

REVIEW

Licensing the Mizar Mathematical Library

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 1107.3212 v1 pith:OO47C4BO submitted 2011-07-16 cs.DL cs.MS

Jesse Alama , Michael Kohlhase , Adam Naumowicz , Piotr Rudnicki , Josef Urban , Lionel Mamane This is my paper
classification cs.DLcs.MS
keywords mizarcommunitymathematicallibraryauthorsbeencopyrightformalised
verification ladder T0 review T1 audit T2 compute T3 formal
0 comments
read the original 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.

Discussion (0). Sign in to comment.

Pith tools