MathWiki conference III

Aarne Ranta on Formal Mathematics in Informal Language

This talk considers generating readable prezentations of formalized mathematics as a special case of parsing and generating natural language statements. It looks like the idea is to translate at least formal definitions and statements, and perhaps also proofs, into the GF language, then generate natural language(s) reprezentation from that.

The talk is more about computer-supported linguistics than mathematics so I don’t want to pretend I understand what is on the slides. Some interesting comments from the author can be found on his blog.

Cezary Kaliszyk on teaching logic using web interface for COQ

The slides are actually about a bit more than the title says. Cezary’s web interface to provers is the closest thing to the formalized math wiki that exists. It is quite generic and besides COQ it supports (at least) Isabelle back end. It even supports Isabelle/ZF so it already can be used for learning the prover without having to install it. I was not able to verify IsarMathLib theories though as the interface seems to have problems with mixing formal text, informal text and comments.

MathWiki conference II

Christoph Lüth on PGIP

PGIP is a protocol for communication beween a proof assistant front end (editor) and a theorem prover. It seems that in practice at the moment it is used only by Proof General front-end to talk to Isabelle prover. I am using XEmacs based version of Proof General and I am quite satisfied with it. Through some wizard-level hackery the PG developers managed to coerce Emacs to display subscripts and some mathematical symbols, so it is almost WYSIWYG.

One of the slides from the talk is a screenshot of the new generation of Proof General, based on Eclipse. Eclipse is more known as a platform for software development tools rather than document creation tools, so I was afraid it would be a step back as far as formalized mathematics is concerned. But from the slide I can see that there will be some mathematical symbols support. Hopefully all those gadgets around the main editing frame can be turned off and the new PG will be at least as good as the old one.

I am curious what was the rationale for selecting Eclipse for the Proof General basis, instead of for example creating a GNU TeXmacs PGIP plugin. TeXmacs has excellent support for mathematical typesetting and is specially designed to be a front end to other programs, currently mostly Computer Algebra Systems.

Herman Geuvers on Wiki for formalized mathematics

I think this was the most important talk on the conference. Herman Geuvers discussed the plan for getting the EU taxpayers money to finance the development of a formalized mathematics Wiki.

I really want this project to succeed. Writing formalized mathematics is fun, but I imagine doing it in a collaborative Wikipedia-like environment would be much more fun.

In my opinion one of the main obstacles for such Wiki is that most theorem provers don’t support generating readable presentations of formalized text.

“Readable” means different things to different people. For some people “readable” means “looks like Lisp”. Here by “readable proof” I mean one that uses standard mathematical notation and terminology and anyone with some mathematical education is able to follow it without having to learn a new language with words like “constdefs” and “assms”.
The author seems to realize the problem, but the solution that is suggested in the slides is wrong. The idea for the solution is that the formalized math Wiki would contain lots of nicely typeset informal math content so that it can compete with Wikipedia or MathWorld. Then, as soon as an unsuspecting visitor gets lured to the site she would be flashed with a formal proof that looks like this:

intros k l H; induction H as [|l H].

intros; absurd (S k <= k); auto with arith.

destruct H; auto with arith.

(this is taken from Freek Wiedijk’s slides).

I am not against informal text. In fact, most of the volume of IsarMathLib proof document is informal. Just like a standard math paper needs more than just definitions, theorems and proofs, formalized math text needs some informal text to dilute content, explain motivation, mention other people’s work or simply provide keywords to make searching easier. However, this should not be the main ingredient. The approach that reduces formalized text to an optional comment on the informal content misses the point. If a prover does not feature generating readable presentations, it is simply not suitable for formalized math Wiki.

I certainly hope that I am misunderstanding Geuvers’ vision. My opinion is mostly based on a (mockup?) slide with screenshot of a prototype of such Wiki that is included in the talk, so this is very little information. I really wish this project to be a success.

To be continued …

MathWiki conference I

To my delight I have found that the all presentations from the TYPES topical workshop “Math Wiki” that took place in Edinburg, Oct 31 - Nov 1, 2007 have been posted on the web. This is a lot of interesting reading on formalized mathematics. I will discuss some of my impressions here.

Klaus Grue on LogiWeb

This is a description of LogiWeb - a system for … I don’t really know. My first impression was that it is kind of like Hilbert II - another project building infrastructure for formalized mathematics that asymptotically approaches the difficult part in its lifetime - actually formalizing the math and creating libraries. However after looking at the objectives (fundationally agnostic) and an example proof (very low level with no prover support) I started to think that this is how Metamath would look like if Norman Megill had spent all these years writing software for formalizing math instead of creating formalized math.

As I was reading the presentation trying to understand what LogiWeb is I had more and more problems in putting some bounds on what LogiWeb can do. It has a built-in version control (or rather package management) that allows to maintain consistency of changing interdependent knowledge representations (very good idea). It can output (”render”) files in .html, .xml, .lisp, .exe formats and in fact any other format. It can create “Logiweb machines” that are Turing-complete and support input/output capabilities, interrupt handling, distinction between supervisor and user-mode and non-preemptive scheduling. Logiweb machines can run real-time, safety critical software. As for formalized mathematics, LogiWeb can support Peano Arithmetic as well as mainstream theories like FOL, PA, ZFC, NGB and so on. That’s all great but I have a feeling that Klaus Grue uses the word “can” in a rather metaphoric way. He should really be saying “potentially can” to be more clear.

To me software for doing formalized mathematics becomes interesting when:

1. it supports ZF set theory or something similar (really, now, not potentially),

2. some work has been done on formalizing a bit more than foundations so that I can evaluate how readable the proofs can be made and how easy they are to write.

It looks like LogiWeb is not at this point yet.

Adam Naumowicz on Mizar

Mizar is still the best tool for a mathematician to do formalized mathematics. Online interface? Mizar has had it for a while now.

Too bad Mizar is not free.

Carsten Schürmann on Logosphere

Logosphere is a formal digital library project developed (mostly) by Department of Computer Science of Yale University.

Logosphere’s approach reminds me a bit of Sage - a very succesful mathematical software project which is based on integrating existing tools rather than inventing new ones, as they call it “Building the Car Instead of Reinventing the Wheel”. Similarly Logosphere tries to serve as a common platform for translation between different theorem provers.

Schürmann prezentation contains a very informative picture on different logical frameworks and provers that support them. This brings up the question - which foundation is the best for a community based formalized mathematics wiki project? In other words, which foundation has a best chance to attract a significant number of contributors?

I think there is a big difference beween the view on foundations of mathematics among mathematicians and computer scientists. If someone made a survey at a math department asking faculty a question on what mathematical foundation their work is based on, I am sure most would answer “ZFC”. The majority of the remaining ones would say that they don’t care because it does not play any role in their work or say something generic, like “logic and set theory”, just because they are not even aware there is something else than ZFC. The majority of the remaining ones would declare that they work in category theory or maybe something more exotic like that they are constructivists.

Over at the computing science department the situation would be quite different. ZFC is not good for formal software verification or modeling computation. As a result there is much greater variety of logics and type theories that count as foundations for computer scientiststs. Theorem provers are typically created at computing science departments. No wonder that so few provers (Isabelle and Mizar) support ZFC.

Another reason support for ZFC is rare is that funding for formalized mathematics projects is often obtained by promising something like “the production of mathematically proved programs” (Cornell, NuPrl, grant from the Office of Naval Research). Once your stated goal is formally verified software, ZFC is gone from the picture, together with a chance for a larger participation of people with standard mathematical education .

I am a mathematician by training and I have tried to use Isabelle/HOL. It was weird and I felt like I was writing software rather than mathematics. I could do it, but it was not fun. Isabelle/ZF, on the other hand was easy and natural. That’s why IsarMathLib is a library for Isabelle/ZF, not Isabelle/HOL.

To be continued…