[FOM] Beautiful Formalization Project.

[Freek Wiedijk]

Merlin:

>There is an ongoing project in this direction called
>"Naproche" (for "Natural Language Proof Checking"),
>initiated and led by Peter Koepke from Bonn and Bernhard
>Schröder from Duisburg-Essen: http://naproche.net/index.php

Another system that might be interesting in
this respect is Andrei Paskevich's ForTheL, see
<http://nevidal.org/download/forthel.pdf>.  I would really
like to know what Harvey thinks of the syntax of the examples
in the appendices of that paper.

And, in case it hasn't been mentioned yet,
there is of course "The Language of mathematics"
<http://link.springer.com/book/10.1007%2F978-3-642-37012-0>
by Mohan Ganesalingam, see also the slides
<http://people.ds.cam.ac.uk/mg262/CSLI%20talk.pdf>.

Personally I find ForTheL more interesting than Naproche and
Ganesalingam's system (even though linguistically those are
major effors).  Having a computer make sense of the fuzziness
of natural language doesn't appeal to me.  As a mathematician
I would prefer _not_ have to deal with fuzziness at all.
So I don't mind using a good "controlled" language.  But the
question then will be: when is it good enough?  I guess.

Freek