Proofs are one of the defining features of mathematical content: practically any mathematical work is considered incomplete without a proof. A “proof” of a mathematical fact is a clear explanation of why the fact is true, starting from some previous known facts and agreed-upon definitions.
When I initially started up Groupprops, my idea was to create a repository of basic definitions of mathematical terms, organized using the property-theoretic paradigm. Proofs had a secondary role, and I initially didn’t intend to put separate pages about facts. however, within a month or so of editing, I realised the importance of having separate pages about facts. A fact here refers to a precisely formulated mathematical statement that has a proof. Each of the fact pages has its proof section.
Over time, I have worked to improve the fact pages to make them more useful and more actionable. Consider a wide range of fact pages in Groupprops: characteristic implies normal, normal not implies characteristic, normality is not transitive, equivalence of definitions of group are some starting examples. A categorized list of facts and a complete list of all facts, for those who want many more.
This subject wiki page describes the general layout of fact articles. In this blog post, I’ll explain a bit about why I’ve made certain choices about designing fact pages.
The first maxim I’ve tried to follow is that for simple but extremely important facts, I’ve striven to provide complete, hands-on proofs. This is so even when the proof is obvious or follows directly from some other proof. The reason is that a lot of time, a learner or researcher tends to get confused about a simple fact, and looking up a simple proof quickly can help dispel the confusion.
Second, in most cases of simple but important statements, I’ve also tried to provide alternate proofs to the hands-on proofs. Usually, these alternate proofs aren’t different: they juts couch the hands-on proofs in a slightly different formal language that enables different directions of generalization. The characteristic implies normal page is an example.
In some cases of complicated statements, a hands-on proof (That assumes very few basic facts) is accompanied by another proof that simply combines a list of other facts — esentially a breakup of the proof. This gives learners flexibility between reading the direct proof and understanding the different components of the proof in a modular fashion. Learners who want to generalize some of the proof ideas may prefer the modular fashion. Learners who just want to understand the proof without being burdened by too many special ideas may prefer the hands-on proof. Of course, even learners who want to generalize the idea may prefer the hands-on proof if the way they’re generalizing is orthogonal to the way the breakup is done.
Third, for facts whose proofs use other facts, there is a “Facts used” section that lists all the other facts that need to be used for the proof. These are numbered and the facts are referred to by number in the actual proof. The main advantage I see for this is that even people who do not want to go through the proof can eyeball and get an idea of what facts are used in the proof. Here’s an example of the critical subgroup theorem where the list of facts used is rather long.
This is in contrast with textbook proofs and the typical presentation style of proofs, where the list of facts used is typically not stated before the proof, but rather, the facts are referred to by theorem or lemma number within the proof. I think the approach used in the subject wikis is clearer particularly when the facts used are of a diverse range. It’s also more suited to a wiki, that thrives on links, as opposed to a sequenced text, that is based on the order in which material appears.
A fourth thing I’ve tried to do is that, for step-by-step proofs that involve arguments within arguments, I’ve used an enumerated point presentation. Enumerated points allow one to refer more easily to previous steps. Further, the enumeration enables people to get a sketch or outline of the proof, because in most cases, I begin the enumerated point with a statement of the goal of that point. Thus, people can just read the goal of each point and get an idea of the proof direction. Learners who want to get practice with proving stuff can note down the goal of each point and then try to fill in details themselves without looking at what is given.
Fifth, most fact pages have lists of related facts, which include generalizations, applications, corollaries, similar statements, opposite statements, and other facts using similar proof ideas. They also give the proof in multiple versions, often using different notations (for instance, one proof using the left-action convention, another using the right-action convention). Finally, for proofs that are particularly easy if specific definitions are chosen for the terms involved in the proof, a separate section called “Definitions used” is present that describes the definitions of the terms used in the proofs.
Arguably, a disadvantage of these is that even simple facts that usually merit only a couple of lines (not even a formal proof) often have extremely long pages on the wiki. I don’t consider this a disadvantage because, in my experience, the simplest ideas are often launching pads for more complicated questions. If the content of the page provides a large number of starting points for further research, I think the goal of having a wiki page on such facts is meant.
Another thing I’ve tried to do systematically is to treat counterexample pages at par with proof pages. Many mathematical facts are essentially just counterexamples to theorems that we might have hoped for. For instance, normality is not transitive. But each of these gets its own page just as much as the theorems do, even if the “proofs” of these essentially just involve describing one counterexample. Thus, for instance, Category:Subgroup property implications, which lists implication relations between subgroup properties, has a counterpart, Category:Subgroup property non-implications, which lists statements about implication relations that do not hold.
In the offing now are ideas about how to make proofs more interactive and actionable. For counterexample pages that can be verified computationally using software such as GAP, I’ve tried to give short GAP code that allows people to “check” the counterexample. This includes both specific counterexamples and general classes of counterexamples (see, for instance, the GAP implementation in normality is not transitive). My goal is to make this available for all specific counterexamples.
GAP-actionability would also be good even for theoretical proofs. For instance, there could be situations where key ideas in proofs can be illustrated computationally.
Another idea is to provide flow diagrams that encode the proof, particularly for complicated proofs. I don’t yet have samples of this.
A third idea, that I have partially implemented, is to guide readers towards general survey articles that discuss the fact as well as the ideas behind the proof. Some of these survey articles specialize in knitting together the different facts known about certain kinds of things, as well as how the proofs of these facts follow from some general ideas and from each other. Other survey articles specialize in proof techniques that apply to a wide range of things. In the former category is an article such as deducing basic facts about Sylow subgroups and Hall subgroups and in the latter category is disproving transitivity.
I’ll be interested in seeing how these ideas work out, and whether they work well on the other math subject wikis.