Metamath Home Metamath Web Site - Copyright Terms  
Mirrors  >  Home  >  Copyright Terms

Most Databases - Public Domain

All Metamath databases (the *.mm files in the Metamath program download, where "*" matches any character string), except for the one mentioned below, are waived of all rights, including copyright, according to the CC0 Public Domain Dedication [accessed 17-Aug-2018]. A comment at the top of each database indicates its copyright status.

Exception. The database file (Peano arithmetic) is copyright by Robert Solovay under the terms of the GNU General Public License.

Most Software - GPL

Unless otherwise stated, the software on this site (C, Java, and Python programs) is copyright under the terms of the GNU General Public License Version 2 or later.

Exception. The eimm program, including its source code, is placed in the public domain.

Some Web Pages - Open Documentation Licenses

If not otherwise stated on the pages themselves, the web pages on this site are available under two licenses: GNU Free Documentation License [accessed 17-Aug-2018] 1.2 or higher and the Creative Commons Attribution License [accessed 17-Aug-2018] 2.5 or higher. You may choose whichever license you prefer.

Some Web Pages - Public Domain

Certain web pages, or parts of web pages, are placed in the public domain by the author, Norman Megill, and other contributors if any, per the CC0 Public Domain Dedication [accessed 17-Aug-2018], when explicitly stated in a notice at the bottom of the page.

The public domain release applies to the original content on those pages, which (to the author's best knowledge and unless stated otherwise in the notice at the bottom of the page) is all text and images displayed on the page other than any short attributed quotations from copyrighted sources.

The public domain release applies worldwide. In case this is not legally possible, the right is granted to use the work for any purpose, without any conditions, unless such conditions are required by law.

Metamath Logo

In response to some inquiries, the image used for the Metamath logo is specifically placed in the public domain. In other words, you are free to sell coffee mugs or tee shirts with the logo without paying royalties or acknowledging its source. Higher-resolution versions are available as mmlogo.svg (courtesy of Giovanni Mascellani) and mmlogo.gif. If you wish to credit the image, "Credit: N. Megill (1994) and G. Mascellani (2019). Public domain." is suggested. A logo with the Metamath name is mmlogotitle.svg (courtesy of Giovanni Mascellani).


Some web pages on this site may contain trademarked names or icons. These belong to their respective owners.

The name "Metamath" has been used publicly by Norman Megill since 1994 to refer to a computer language and related software.

Note for Contributors

You are asked to place in the public domain any contribution you make to the various databases, so that the databases can remain public-domain documents. (If you wish to retain copyright to your work, you are free to branch a public-domain database into a copyrighted work of your own.)

Ordinarily, I will request that any patch or enhancement to a program I have written be placed in the public domain, because eventually I may place the program in the public domain. (If you wish to retain copyright to your patch or enhancement, you are free to branch the program into your own version with a compatible copyright license.)

(End of Copyright Terms)

Editorial Comment on Public Domain

After considering a number of copyright licensing alternatives, I have concluded that for mathematical proofs, public domain is in the best spirit and tradition of mathematics. This is a personal decision, but I think that acknowledgment of my work is best dealt with through courtesy and ethics rather than under threat of a lawsuit, which is what a copyright license essentially entails. Plagiarizers will have their own consciences (and reputations) to deal with, and I have more important things to do with my time than to worry about them.

Ultimately I can envision mathematical proof databases that will be shared and built on, and there can be gray areas as to what constitutes a copyright contribution. For example, if a proof is shortened or rewritten completely, at what point does the original contributor's "ownership" cease? Or proofs may be merged together, or a theorem may be restated and reproved in a more convenient form, ideas or pieces of one proof may be borrowed for use in another, and so on.

A public domain proof database provides complete freedom from distraction by such issues, allowing all effort to be focused on the mathematics itself. Anyone can purge things, clean up comments, revise theorems, and make use of it any way he or she sees fit without fear of violating the fine print of a contract, license, or law. Professional courtesy demands acknowledgment where appropriate and practical, but in my view this should be a matter of ethics and common sense rather than law.

A mathematical result per se cannot be copyrighted, only its presentation. The existing communication channels and peer-reviewed journals already ensure proper credit for significant mathematical discoveries, and journal publication establishing precedence will usually happen well before formalization into a computer database. If, in the distant future, computer-verified databases become a primary means of communication, in principle they can be registered with a trusted authority to establish precedence and still be placed in the public domain. Public domain ensures that others are unencumbered to freely build on the work and maximize the rate of progress in the field. This is what already happens informally now. In present-day mathematics, falsely claiming credit for someone else's discovery is an ethical violation that is rarely pursued legally; instead, the punishment that effectively results from a tarnished reputation is already a severe one.

The founders of the QED Project [accessed 17-Aug-2018] also considered public domain important for its purposes. The goal of this project is to build a comprehensive repository of computer-verified mathematics. From the QED Manifesto [accessed 17-Aug-2018]:

Objection 2: Intellectual property problems. Such an enterprise as QED is doomed because as soon as it is even slightly successful, it will be so swamped by lawyers with issues of ownership, copyright, trade secrecy, and patent law that the necessary wide cooperation of hundreds of mathematicians, computer scientists, research agencies, and institutions will become impossible.

Reply to Objection 2: In full cognizance of the dangers of this objection, we put forward as a fundamental and initial principle that the entirety of the QED system is to be in the international public domain, so that all can freely benefit from it, and thus be inspired to contribute to its further development.

Valid HTML 4.01!
This page was last updated on 5-Jun-2019.
Your comments are welcome: Norman Megill nm at alum dot mit dot edu