ProofWiki:Current events/ITP 2011

ITP 2011: Conference Report

It was noted how similar in intent, if not execution, $\mathsf{Pr} \infty \mathsf{fWiki}$ is to PlanetMath. This was seen as being a Good Thing, in that it can be used as the basis for considerable collaboration.

We briefly discussed the idea that $\mathsf{Pr} \infty \mathsf{fWiki}$ and PlanetMath might merge at some point, -- but at present the idea we're most interested in exploring is plentiful cross-linking to offer better mutual support. I note that this is starting to happen already - the (current) latest entry on PlanetMath responds to a question which is raised on $\mathsf{Pr} \infty \mathsf{fWiki}$; and there exists a template in $\mathsf{Pr} \infty \mathsf{fWiki}$ allowing direct linking to PlanetMath.

Joseph Corneli, one of the movers and shakers at PlanetMath, is doing a research project on aspects of math wikis (details at http://metameso.org/~joe/thesis-outline.html). During the course of discussions he and I had over the course of the weekend, the following suggestions and intentions were expressed:

Respect

$\mathsf{Pr} \infty \mathsf{fWiki}$ appears to be treated with considerable respect within the MathWiki community. It has aspects which appear to be unique and compelling, and it is doing something which no other site does, and by all accounts, it seems to be doing it well.

Internationalization

This has already been mentioned in $\mathsf{Pr} \infty \mathsf{fWiki}$, and is an outstanding question on the main page. The consensus at the time was that yes, this would be a good idea, but may be too much like hard work at the moment.

However, we might be able to make a start. Definitions, for example. It was suggested that on each definition page we might include the name for the concept being defined in whatever languages we can muster, or that are considered "important", e.g. French, German, Russian, Latin(?), Italian, and whatever other main languages have consistently been used for presentation of mathematical papers.

The example of "local field" being "corps local" in French (literally: "local body"), while the "natural language" translation of "field" into French translates back into English as "meadow" is a case in point. So using an ordinary dictionary There appears to be no on-line dictionary for the translation of mathematical terms. It would be good for one to be developed.

Making the proof structures more rigid

We are already most of the way there with this one. All proofs are written in simple sentences, the shorter the better, and simple "modus ponens" style compound statements, for example:

Let $A$ be a $B$.

Let $C$ be a $D$.

From the result "All $B$ are $D$", it follows that $A$ is a $C$.

(Yes I know the above does not logically hold, this is just an example of style.)

In more extreme cases the entire proof is done symbolically in an "eqn" template structure.

One big suggestion was that this may make it considerably easier for $\mathsf{Pr} \infty \mathsf{fWiki}$ to be interfaced with an automatic theorem prover (which was the main purpose of this conference, to bring together the threads of the research which has been done over the last 40 years or so). Already this structure is compatible with tools such as "Mizar" (I'll look up a link to it later) and research should be done to see how such an interface may be accomplished.

More to the point, as the structure is so rigid, it should be possible to further enhance the automatic structuring of our pages, for example by expanding the concept of the "eqn" template to encompass proof lines written in "natural language".

What all this means is that our "terse" house style would need to be rigidly enforced throughout. This is actually de facto as it stands, as every page written is near-enough immediately restructured as it comes in. So it is considered more than just an idiosyncrasy, it is being viewed as an essential part of $\mathsf{Pr} \infty \mathsf{fWiki}$'s philosophy by those who are coming to take it seriously as a valuable addition to the mathematics.

Copyright Policy

We are currently running with th GNU FDL licence. It has been suggested that we amend this to a Creative Commons license. There are many of these available to use, but two interesting ones are:

• CC0: Any material appearing here is considered to be free and available to be used by anybody.

• CC-By-SA: Allows any material to be used by anyone, as long as its source is cited. (This is the license that is used by PlanetMath, and by Wikipedia.)

I know nothing about the legal aspects of copyright policy (beyond expressing an opinion that in this context they get in the way of the spread of mathematical knowledge), but what I would encourage is that we adopt one whereby everything is as freely accessed as possible. However, if we were to change the policy from GNU FDL, we would need to consult all the contributors (or major contributors) to ask whether they would be okay with this change.

This may not be a particularly arduous thing to do, considering that most of the mathematics on this site has been around for so long that it's bound to be public domain anyway.

Watch this space, as there may well be suggestions for enhancements in this area.

Sources, and the Learning Experience

We had a discussion about how we learn mathematics. How do we "learn" mathematics? We don't know - if we did we'd bottle it and sell it.

But the usual concept is that we get a book and work through it from page one to page $n$, linearly. $\mathsf{Pr} \infty \mathsf{fWiki}$ / PlanetMath etc. have no such linearity. But its very lack of linear structure is in some ways a limitation.

It is noted that the source works from which the pages have been constructed are added at the bottom. It would not take too much effort to add a "next / prev" link to the "BookReference" template so as to provide a direct link to the next proof / definition in the book, for each book in question. Then the linearity of the book structure can be exploited, and a user may be able to follow the course of study for any given book.

Obviously the pages in question are more than just the content of the books, so any such path will provide a significantly richer learning experience than would be obtained by just following the book.

Exercises

Something else we've touched upon in the past. We may want to develop a standard technique for adding exercises to the various proofs and definitions. The thinking behind this is still seriously a work in progress.

Okay, that's some of the stuff we discussed. I'll get back to this in a while.

--prime mover 13:55, 29 August 2011 (CDT)