ProofWiki Matt Westwood 1 Introduction ProofWiki is an online repository for mathematical proofs. Its stated mission is: “the collection, collab- oration and classification of mathematical proofs.” To that end, it provides: • A catalogue of definitions of mathematical concepts, categorised according to context (e.g. topol- ogy, number theory, analysis, graph theory, abstract algebra). • A catalogue of axiomatic frameworks (e.g. Zermelo-Fraenkel axioms, axioms for Natural Deduc- tion in the context of propositional logic, etc.) • A repository of mathematical proofs, categorised, like the definitions, according to context. • A rudimentary historical context, in the form of short biographical pages arranged into chronolog- ical order, in which the intention is to provide links to the original source works in which particular pieces of work first appeared. • A glossary of works from which the material was sourced. It can be found at www.proofwiki.org. ProofWiki Westwood 2 History ProofWiki was conceived by Joe George, a student of mathematics at the University of Newfoundland, and set up in March 2008 by him with the help of a couple of friends. Over the last three years it has been accumulating users steadily, until now there are over four hun- dred. The author became involved in July 2008, having been alerted to it from mathhelpforum, to which he was a regular contributor. The author had a wealth of mathematical material which had been assembled in LATEX format over several years, but had been struggling to find a way to present it on the Internet. The still-embryonic ProofWiki appeared to be exactly the medium for presenting the accumulated material in the way it had originally been envisaged. Since that time, the author has spent considerable time building up the site and contributing to the direction of its evolution. 2.1 Statistics The following numbers may be of interest. They are accurate at the time of writing (5th July 2011): • Number of proofs: 3795 • Number of definitions: 2819 • Number of users: 426 • From Google Analytics, between 4th June and 4th July: – Number of visits: 35,850 – Number of pageviews: 88,866 – Percentage of new visitors: 74.71% 2.2 Philosophy A mathematician’s work consists of proving things. How useful would it be, one would ask, to have a compendium of proofs of all sorts of standard results? No comprehensive website exists, we believe, dedicated entirely to the documentation of actual proofs of results. There are plenty of sites replete with definitions, but as far as we know, no site had yet been created with the express purpose of providing the proofs themselves. Into how much detail should a proof go? Many published proofs contain phrases such as “It is easy to see that . . . ” or “It obviously follows that . . . ” and so on. It is the philosophy of ProofWiki to include all these skipped-over parts. Every step of a proof should be documented, and every concept defined. We consider that every page should ultimately be accessible to any reader who reaches such a page. The only barrier to comprehension is an understanding of the concepts. To that end, every single technical term is provided with a link to a page defining what it means. It can be argued that the very existence of ProofWiki is a Bad Idea. In order to become a mathe- matician, one is supposed to be able to prove things. Much of the work of a mathematics undergraduate student consists of creating such proofs, from whole cloth, in order to develop the skills to progress. If such proofs are freely available on the Internet, and can be directly cut and pasted into place into an assignment document, then where is the benefit to the student? This paper does not attempt to argue this point, beyond making the observation that all such ency- clopedias cause exactly the same concern to be raised. ProofWiki Westwood 3 Structure ProofWiki has been constructed with the following philosophical strategies in mind. 3.1 Separation of Definitions and Axioms from Proofs Because a definition is a completely different concept to a proof, an early decision was made to separate the various categories of entity into separate namespaces. These über-categories are available directly from the main menu sidebar, and can be browsed as follows: • Proof Index • Definition Index • Symbol Index • Axiom Index ... and so on. There are other miscellaneous namespaces which are 3.2 Deep levels of categorisation When you are crafting a proof in a particular field of study, you have a convenient folder where you can find any existing results relating to a particular definition. Take for instance: Arens-Fort Space is Completely Hausdorff. This result goes directly into two categories: • Category:Arens-Fort Space • Category:Completely Hausdorff Spaces. In turn: • “Category:Arens-Fort Space” is in Category:Examples of Topologies. • “Category:Examples of Topologies” is in Category:Topology • “Category:Topology” is in: – Category:Proofs – Category:Set Theory – Category:Analysis • “Category:Set Theory” is in Category:Proofs • “Category:Analysis” is in Category:Proofs From the other path: • “Category:Completely Hausdorff Spaces” is in Category:Hausdorff Spaces. • “Category:Hausdorff Spaces” is in Category:Separation Axioms • “Category:Separation Axioms” is in Category:Topology ... and so on. ProofWiki Westwood 3.3 Accurate and meaningful page names There is a fine line between being too terse (thereby making it obscure) and being too wordy (thus making the category page more difficult to scan). We also try to use a “name” for a result, if it exists (and we can find out what it is). As ProofWiki has evolved, so have the page names. As an example, the following pages names have all been used for the Odd Number Theorem: • Recurrence Formula for Square Numbers • 1 + 3 + ... + (2n − 1) = n2 • Sums of Sequence of Odd Numbers • Sum of Sequence of Odd Numbers Each of the superseded page titles have been kept as a redirect. 3.4 Short and pithy pages Some wiki sites on the internet (in particular Wikipedia) try to make a page as comprehensive as possible: with a history, a list of examples, a paragraph of applications, a full dissertation of which directions research has taken the subject, and of course a summary for the lay person. ProofWiki’s philosophy is: less is more. If you have a great deal to say, then split it into several pages. One page: one result. One page: one lemma. One page: one specific example. (MediaWiki applications encourage the use of shorter pages anyway — if you write a page with over thirty thousand or so characters, it issues you a warning.) Some topics, however, have many different aspects to them, to such an extent that to write these aspects all into the same page would cause that page to become larger than is desirable. ProofWiki has a way around this problem: using the inbuilt “transclusion” tool in MediaWiki, it is possible to construct a large page out of a number of smaller pages. This can be particularly useful when you want to group together many proofs or definitions in one place, but still keep the individual sections as standalone pages in their own right. Some particular examples: • Definition:Separation Axioms • Trigonometric Identities Note how each section title of these pages is a link which leads directly to the subpage from which the relevant parts have been transcluded into the main page. 3.5 A consistent approach to symbology It is appreciated that there is considerable variation between various notations. While it is impossible to cater to everybody’s personal taste in notation, an attempt has been made to establish a notational convention on the site. When a concept is introduced by means of a definition, the various symbols for it are defined (if relevant with a historical perspective), and the ProofWiki preferred symbol is specified. From Definition:Set Complement: ProofWiki Westwood “No standard symbol for this concept has evolved. There are alternative symbols for { (S) and S. C (S) is sometimes encountered, and may appear occasionally on this website. Another common one is S0 , but it can be argued that the symbol 0 is already overused. “Some authors use Sc or S{ , but those can also be confused with notation used for the group the- oretical conjugate. Some authors use CS. Another one is S∗ , and another is S̃. You may encounter others.” An attempt is usually made to use the notation which matches the name of the LATEX tag that defines it, for example A \setminus B for A \ B and \circ \restriction_A for ◦ A . In cases where the notation used is not universally understood, the strategy is for every page which uses this notation to explain it wherever it is used. It is planned (but no work has yet been done on this) for a list of “approved symbology” for the site. Till then we need to be tolerant of variation. The subject is contentious, as different users have their own preferred systems of notation. This is an area where advice may be needed. 3.6 The use of mathematical language over English A specific example is that “iff” is preferred over the more wordy “if and only if”. The disadvantage of this is that casual viewers frequently see this as a typo, and well-meaningly “correct” it. This is alleviated by specifically linking to a page which defines what “iff” actually means. 3.7 A widely spaced presentation A mistake often made in presentation of material for a computer screen is to mistake it for just another page in a book. However, it is believed by the author (and research may back this up) that in order to be properly taken in, information on a screen needs to be far less dense than on the printed page. To this end, a house standard is to present each thought (in most cases that means “each sentence”) on a separate line, with a blank line between it and the next line. More space can be put between rows to emulate paragraphs. Screen space is not paper to be conserved. Screen space is free. An exemplar of this style is the page Big Implies Saturated. 3.8 A historical perspective The mathematicians who have contributed through the ages to this body of learning are credited as far as is known. Sources are documented (although this is currently incomplete) so that the user is able to access the original source material in which a concept is introduced. Variations in approach are documented when appropriate, and contentious and inaccurate statements are challenged. Some exemplar pages: • Definition:Pascal’s Triangle, in which a section of historical notes is included. • Definition:Empty Set, in which an unwillingness by certain authors to acknowledge the existence of the empty set as an object is questioned. • Union of Exteriors contains Exterior of Intersection, in which an inaccurate statement made in a published work is documented. ProofWiki Westwood 4 Infrastructure ProofWiki was constructed around the readily available MediaWiki package (see http://www.mediawiki. org), a popular example of which is Wikipedia. All mathematical material is written in LATEX according to a set of loosely-enforced house rules. This LTEX is rendered by MathJax, which is found on http://www.mathjax.org/. A ProofWiki has never been comfortable when viewed using Internet Explorer. It works, but the layout is compromised. For best results on a PC, Firefox or Google Chrome are recommended. The author has no knowledge of the user experience on other platforms. 5 Comparison with other sites 5.1 Wikipedia See http://www.wikipedia.org. As ProofWiki uses the same architecture as Wikipedia, and has been deployed with little customi- sation of appearance, the two sites have a similar look-and-feel. However, the strategies are markedly different. Wikipedia, as its name suggests, takes an encyclopedic approach to its subject. A page on a given subject is designed to hold as much information as possible, with the result that pages can become so large as to become unwieldy and in extreme cases amorphous. This is in direct contrast to the approach of ProofWiki, in which pages are deliberately crafted to be short and pithy. If there are multiple contexts for a given topic, then it is usual to split these up into separate pages, transcluded into a summary page. The MediaWiki software “transclusion” capabilities have been exploited to a fair extent to allow this to be accomplished. As an example of how transclusion has been exploited, see the entry Trigonometric Identities. Also there is a high-level strategy to include on Wikipedia only “notable” subjects, and to disal- low original research. On ProofWiki no such limitation has been imposed. If a mathematical item is interesting enough for a contributor to spend the time to enter it, then it is deemed worthy of inclusion. Wikipedia is inconsistent in the technique for rendition of mathematical symbology. There is a con- tinual discussion on that site as to whether it is better to use LATEX inline or whether to use conventional html formatting. It is the view of ProofWiki that all mathematics is best rendered in LATEX, in order to achieve full consistency of look-and-feel. On occasion an article which has been slated for deletion from Wikipedia has been rescued and added to ProofWiki. A notable example of this is the entry on Boubaker polynomials, which had a stormy history on Wikipedia and was eventually deleted amidst a squall of wrangling. 5.2 Wolfram MathWorld See http://mathworld.wolfram.com. Wolfram MathWorld is arguably the most elegantly presented and comprehensive on-line mathemat- ical encyclopedia, but then it is perhaps the oldest.1 However, its focus is on definitions only, and no attempt has been made to add proofs. In structure and presentation it closely resembles ProofWiki in its attempt to provide a compact and easily-assimilable page rather than bombard the reader with a large quantity of information. There is also a section on each page containing links to other relevant pages. 1 The author knows of no such older site. ProofWiki Westwood It may well be suggested that the structure of ProofWiki was influenced significantly by MathWorld, but if this is the case then such influence was (at least in the mind of the author) completely unconscious. Having said that, all such mathematics websites, not least ProofWiki, owe a considerable debt to MathWorld for showing what is possible. 5.3 PlanetMath See http://planetmath.org. ProofWiki bears a considerable resemblance in style, if not format, to PlanetMath. The latter has been evolving for considerably longer, so in many places is more comprehensive. However, the emphasis in PlanetMath is on definitions rather than proofs. While such proofs do exist, this is not consistent and therefore connecting the definitions with their uses is less than successful in places. PlanetMath has been configured very much as a community, with an active discussion forum. On each page the author’s username is prominent, as are the statistics for each user’s contributions. Each page has a tool by which feedback may be offered on each page, but whether this is working or not needs to be reviewed. Each page on PlanetMath also has its MSC number2 appended to it. This is still a work-in-progress on ProofWiki. 5.4 The MacTutor History of Mathematics archive See http://www-history.mcs.st-andrews.ac.uk/history/index.html. This is a specialised site whose main purpose is to provide short biographies of all the major math- ematicians in history. As such it has no intention of documenting any of the actual mathematics itself. However, it has been used as a resource for some of the historical detail which is often added to a page to add context. 5.5 Others The author appreciates that there are many other websites out there whose content and approach overlap that of ProofWiki, but there has been insufficient research done in order to provide a worthwhile analysis of them. Their presence is welcomed and supported. 6 Who’s Who Because of its nature, nothing is known about the various authors beyond what they have seen fit to publicise. There are three administrator accounts: “Prime.mover”, “Joe” and “Alecscooper”. “Joe” has the responsibility for maintaining the website’s infrastructure, for example, upgrading the MediaWiki software as it becomes necessary. ”Prime.mover” has contributed the bulk of the material on the site so far, and continues active and prolific involvement. “Alecscooper” also contributes as and when his schedule allows, and keeps an eye on the user ac- counts. 2 Mathematics Subject Classification ProofWiki Westwood 7 How To Contribute ProofWiki has been set up to be completely free access. Anybody accessing the website has authority to add or amend any page at all. You do not even have to create a user account, although if you are preparing to contribute a significant quantity of materials you are firmly encouraged to do so. This potentially leaves us open to all sorts of abuse to vandals and spam-merchants. However, this is guarded against by two so-far foolproof techniques: 1. A mathematical captcha: anonymous users are expected to solve a simple addition/subtraction test to prove they are not robots. While this looks as though it should be pitifully simple to subvert, so far it has worked. 2. The permanent disabling of perpetrators’ accounts. This has been done in the past where users have set up accounts as a means to provide links to websites dedicated to non-mathematical activities (macramé, anti-smoking, political propaganda, and so on). It has also been done where users have performed acts of vandalism.3 Not only can the user account be blocked, but so can the IP address from where the dodgy account was set up. The main reason why this technique has proved successful is because the level of traffic is low enough for one person to be able to monitor it completely. 8 Conclusion The aim to provide proofs of every mathematical result ever published is clearly ambitious. The main limitation to our efforts is no more and no less than mathematical ability. We need people who have the skills to be able to fill in the gaps. There are far too many “stub”, “work in progress” and “explain” pages that need to be completed. 8.1 ProofWiki constantly evolves New results and interesting snippets are added as the contributors discover them. The readership grows wider, and ideas are continually being added for how to improve the presentation. Some may be good, some may not be so good — but the important thing is that the ideas are flowing. 8.2 There are no unbreakable rules And that’s another one. Most of rules and guidelines described in the structure section of this paper have been broken during the course of ProofWiki’s evolution, sometimes because the page breaking that rule was written before the rules had evolved, and sometimes because in a particular context it “made sense at the time”. Sometimes a page is written by a person who does not quite grasp the philosophy upon which ProofWiki emerged (“it thinks, therefore it is”) — such pages stand as they are until they are rebuilt. Sooner or later. 3 A case in point was where a user had a vendetta against another user, and made insulting and demeaning additions to various pages associated with that user. In that case the user, having been blocked, sent an email to the administrators begging to be allowed back on. The block was lifted, and the user continued to perform his childish acts of vandalism, for which his block was reinstated and set to last indefinitely. ProofWiki Westwood 8.3 ProofWiki is for everybody All levels of mathematical literacy are catered for: from the straightforward simplicity of some of the proofs of Pythagoras’ theorem to the forthcoming (planned — don’t hold your breath!) full detail of Fermat’s Last Theorem. Join in!