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…