[FOM] Beautiful Formalization Project.

[Merlin Carl]

> 2. Design a language for presenting proofs that is general purpose
> enough to be used in all three of these contexts.
> 3. The language for presenting proofs should also be accompanied by
> software implementing certain algorithms. This is explained carefully
> below.
> 4. The three texts are written in the language, with ABSOLUTELY
> RIGOROUS MACHINE CHECKABLE PROOFS.
> 5. The resulting three texts are viewed as BEAUTIFUL by all readers.

> 6. Brilliant naive young people cannot tell that these were created in
> the Beautiful Formalization Project.

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
It is developed and described in detail in the PhD thesis "Proof-checking mathematical texts in
controlled natural language" of Marcos Cramer, which can be found here: http://naproche.net/downloads/2013/doktor.pdf

A sample text from the early days of Naproche contains a reformulation of the first chapter of Landau's "Grundlagen der Analysis" ("Foundations of Analysis"): http://naproche.net/downloads/2009/landauChapter1.pdf


This may not yet have reached the point of being regarded beautiful by all readers and when presenting e.g. Theorem 9 along with the "official" translation, most people guessed correctly which was what.

Some time ago, I wrote a text called "Introduction to elementary number theory for humans and machines" that I planned to reformulate in the Naproche language, but so far didn't due to lack of time. Even if this was done, there would, of course, still be a long way to go before one can do this with the average undergraduate textbook with their use of drawings, appeals to intuition, leaving steps as exercises etc.

Best wishes
Merlin Carl