Posts Tagged ‘reviews’

IsarMathLib 1.9.0 released

July 26, 2013

I have released version 1.9.0 of IsarMathLib. This is a quite large release with 10 new theory files and 155 new theorems, all contributed by Daniel de la Concepción Sáez. The first of the files contributed by Daniel (released in 1.8.0), Topology_ZF_4 about nets, filters and convergence in topological spaces is now presented on the site. The rest of Daniel’s contributions for now can be viewed in the proof document and the outline.

Here is a short description of what is in the new theories:



The mathematical truth is out there…

July 19, 2008

The recent issue of Notices contains an opinion piece by Melvyn B. Nathanson titled “Desperately Seeking Mathematical Truth”. The contents of this article can be summarized in the statement “Many (I think most) papers in most refereed journals are not refereed.” . This is the boldest public admission of the state of affairs from a mathematician I have ever seen.


MathWiki conference III

January 13, 2008

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

January 5, 2008

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 …