Bengt Nordström and I went to the MathWiki workshop

http://homepages.inf.ed.ac.uk/da/mathwiki

in Edinburgh. It was organized within the European TYPES programme

http://www.cs.chalmers.se/Cs/Research/Logic/Types

which Bengt coordinates. Since 1993, I used to go to Types meetings regularly. In the last three years, however, other things have prevented me from attending them, so it was nice to see all these colleagues again and get an update of those aspects of Types which are maybe the closest to my current interests.

The workshop served the dual purpose of presenting work and preparing a new European proposal. The proposal had been very well initiated by the Nijmegen group, in the coordination of Herman Geuvers. That discussion was placed in breaks and short intervening sessions, and the talks - some of them by guests from outside Types - completed and inspired the discussions in adequate ways.

For me, the key question was what role natural language could play in a Wiki for formalized mathematics. I'm interested in finding applications for GF (http://digitalgrammars.com/gf), and this has been encouraged by the experience from the WebALT project (http://webalt.math.helsinki.fi). How relevant natural language is in a math wiki depends largely on whom one wants to use it. If the wiki is meant just for experts who want to exchange their formal proofs, then it may be adequate to use just the type theoretical formalisms; it is well known that formal proof experts are more comfortable with formal than natural languages, as it comes to expressing mathematics. To motivate the use of natural language, two new kinds of users should be targeted:

• non-experts in formal proofs, who want to get the formulas explained in a language they are used to
• perhaps, experts from different formalisms, who are unfamiliar with the particular notations of the system and want to get a quick summary of results

In the setting of a European proposal, one could point out that non-expert users should not be underestimated: making the results accessible to a wide audience can be an important part of the dissemination plan. One should also bear in mind that most working mathematicians are non-experts in formal proofs, and might become users of the wiki more easily if they did not need to learn a new language.

Quite a few presentations touched upon the use of natural language: in addition to mine, there was Freek Wiedijk's plea that "look is important", Loïc Pottier's Wikicoqweb system actually using natural language rendering (in French),

http://pcmath165.unice.fr/wcw/spikini/?wiki=AccueilWikiCoqWeb

and Adam Naumowicz's presentation of Mizar, which displayed examples of those very readable Mizar journal articles.

http://mizar.uwb.edu.pl

Most slides are available via the MathWiki abstracts page

http://homepages.inf.ed.ac.uk/da/mathwiki/talks.html

Here is a summary of my conclusions, partly presented in my talk, partly confirmed or inspired by the workshop:

• ordinary mathematical language uses symbolism for some singular terms and predicates, natural language for the overall logical structure and text structure; as a third ingredient, diagrams can be used for presenting sometimes very complex structures
• therefore, to create the "look" of ordinary mathematics, we should present the overall structure in natural languages
• this has been shown feasible as regards definitions and statements of theorems, and also problems and exercises (WebALT): we can translate them mechanically from formal representations to readable natural language
• translating proofs is only feasible if the proofs are structured on high enough level; the main problem in rendering proofs in natural language is largely the same as making them readable as formal proofs (this is a problem especially if the starting point is proofs found by automatic theorem provers)
• from nicely structured proofs, readable natural language can be genererated, as shown by Wikicoqweb and Mizar
• the problem is largely language independent: with a grammar library such as used in WebALT, a solution can be ported to new languages by mainly porting a domain lexicon

In general, the Wiki technology is making entrance in this area, as also shown by the presentations of Cezary Kaliszyk and Pierre Corbineau, reporting on a Wiki and Coq based teaching system ProofWeb,

http://www.cs.ru.nl/~cek/proofweb

In GF, we have taken a step to supporting multilingual Wiki's where the content is stored as abstract syntax in the server and rendered by concrete syntaxes in clients. For creating content, a multilingual syntax editor is provided. The underlying technology is being developed by Björn Bringert and Moises Salvador Meza Moreno. Demos and instructions can be found in

http://csmisc14.cs.chalmers.se/~meza/restWiki/wiki.cgi/

http://web.student.chalmers.se/~meza/

Technorati Tags: MathWiki