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 …