MetamathHome
| Metamath Home |
Metamath Web Site - Copyright Terms |
Exception. The database file peano.mm (Peano arithmetic) is copyright by Robert Solovay under the terms of the GNU General Public License [external].
The software on this site (C, Java, and Python programs) is copyright under the terms of the GNU General Public License [external].
Unless otherwise stated below or on the page itself, the web pages on this site are dual-licensed under the GNU Free Documentation License [external] and the Creative Commons Attribution License [external]. This means you may choose the license that best suits your purpose and disregard the other one, or you may continue to use the same dual licensing.
The web pages generated automatically from the *.mm databases are released to public domain. Specifically, these are the files mmascii.html, mmbiblio.html, mmdefinitions.html, mmtheorems*.html (where "*" matches any character string), and all files hyperlinked from the "Label" column of mmtheorems*.html. These files are present in the mpegif, mpeuni, qlegif, and qleuni subdirectories of the Metamath web site. Examples are the file mpegif/mmtheorems.html and the file mpegif/wn.html hyperlinked from its "Label" column.
Certain other web pages and files may be released to public domain where explicitly stated, for example the GIF and PNG Images for Math Symbols page and its image files.
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 the Metamath software and computer language.
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 for me life is too short to fret 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 a 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.
With public domain there are none of these problems. A public-domain proof database is a completely free collection of bits in every sense of the word. Anyone can go through it and purge things, clean up comments, revise theorems, and make use of it any way he or she wants 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 released to 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 [external] 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 [external]:
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.
