[FOM] 614: Adventures in Formalization 1

[Andrei Popescu]

Dear Harvey,

You wrote:

> Take a look at the statements of theorems in 
> http://www.cs.ru.nl/~freek/100/ They are all unconscionably ugly to 
> read and digest for a typical person outside the Theorem Proving 
> community. In the Theorem Proving community, they are probably looked 
> at as breathtaking works of art.
>
> Now this is something that is a missed opportunity and CAN DEFINITELY 
> BE LARGELY FIXED. Is it worth fixing? ABSOLUTELY, but probably no one 
> in the Theorem Proving community thinks it is worth their time to fix 
> it, and should have a low priority. Conventional wisdom is often very 
> wrong.

Let me just add the following to Dominic's excellent survey: Quite to the opposite, many people in the theorem proving / proof assistant 
community care deeply about, and invest a lot of effort in capturing the mathematician's style of writing proofs.  
As an (IMO) compelling illustration of this effort, please have a brief look at the chapter "Isar: a language for structured proofs" from 

http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2015/doc/prog-prove.pdf

Getting mathematicians to use proof assistants and give their valuable feedback is a major objective of this community. 

All the best, 
   Andrei 




---------------------------------------------------------------------------


Please note that Middlesex University's preferred way of receiving all correspondence is via email in line with our Environmental Policy. All incoming post to Middlesex University is opened and scanned by our digital document handler, CDS, and then emailed to the recipient.
 
If you do not want your correspondence to Middlesex University processed in this way please email the recipient directly. Parcels, couriered items and recorded delivery items will not be opened or scanned by CDS.  There are items which are "exceptions" which will be opened by CDS but will not be scanned a full list of these can be obtained by contacting the University.