|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.
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.
If not otherwise stated on the pages themselves, the web pages on this site are available under two licenses: GNU Free Documentation License [external] 1.2 or higher and the Creative Commons Attribution License [external] 2.5 or higher. You may choose whichever license you prefer.
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 Creative Commons Public Domain Dedication [external], 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.
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.
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.)
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 [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.