[FOM] Adventures in Formalization (Avigad)

[Dana Scott]

In e-mail Jeremy Avigad has written that he is too busy with
the new semester at CMU to post on FOM just now.  He says:

> I have written lots of surveys on the topic already and given 
> talks to a range of audiences, and I don't I have anything to 
> add now.  When the topic came up on FOM last year, Harvey got 
> me to send a message to FOM which has some links that might be
> helpful:
> 
>   http://www.cs.nyu.edu/pipermail/fom/2014-October/018221.html
> 
> Since then, I have also given a series of four talks on formal
> methods in mathematics. They are on my web page under TALKS.
> 
>   http://www.andrew.cmu.edu/user/avigad/
> 
> As to Harvey's specific proposals, a few years ago, an MS student 
> at CMU, Steve Kieffer, implemented Harvey's proposed input language 
> for definitions. You can see some examples in Section 3 of the paper
> here:
> 
>   http://www.andrew.cmu.edu/user/avigad/Papers/mkm/index.html
> 
> The language has some nice features but it is a mess of symbols like 
> any other formal language. Steve and I had the nice idea of allowing 
> users to enter natural-language equivalents for defined functions and 
> predicatse, and we found that we could generate surprisingly readable 
> output:
> 
>   http://www.andrew.cmu.edu/user/avigad/Papers/mkm/munkres.pdf
> 
> As far as parsing natural language input, there have been some 
> experiments with using "controlled natural language," like the one 
> here:
> 
>   http://naproche.net/
> 
> I don't know of any really striking successes. I believe that most 
> people working in ITP find the problem interesting and worthwhile, 
> but don't think it is the most crucial issue facing the subject right 
> now.
> 
> For another experiment, people should also look into Lean:
> 
> Lean is a new open source theorem prover being developed at 
> Microsoft Research, and its standard library at Carnegie 
> Mellon University. The Lean Theorem Prover aims to bridge 
> the gap between interactive and automated theorem proving, 
> by situating automated tools and methods in a framework that 
> supports user interaction and the construction of fully specified 
> axiomatic proofs. The goal is to support both mathematical 
> reasoning and reasoning about complex systems, and to verify 
> claims in both domains.  The Lean project was launched by 
> Leonardo de Moura at Microsoft Research in 2013. It is a 
> collaborative open source project, hosted on GitHub.
>  
>   https://leanprover.github.io/
> 
> There is an online tutorial, which is presented alongside a
> version of Lean running in your browser. The tutorial includes 
> a quick reference. You can explore the standard library directly 
> in the GitHub respository, or through annotated markdown files.