[FOM] Formal verification

[Rempe-Gillen, Lasse]

Thank you all for the many interesting responses to my message. I would like to pick up on a few points.

---
Dominic Mulligan wrote:

> A lack of libraries is a major issue. It's hard to start formalising 
> research level mathematics when large swathes of undergraduate 
> mathematics is still missing from the libraries of the main proof 
> assistants. Further, what exists is coloured by the biases of those who 
> use the systems, mainly computer scientists: there are a lot of 
> formalisations of things like red black trees and typed lambda calculi, 
> for instance, whereas continuous mathematics seems to be neglected, or 
> at least it seems to me.

It always seemed to me naively that it ought to be possible to overcome this obstacle, provided that the right language is around. If one is willing to work with "conditional" verification - which would only require the formalization of the theorems to be used - then presumably it would be possible to formalize results, and fill in the missing links later? 

I for one would also be quite happy to make every beginning postgraduate student of mine - and perhaps also project undergraduate students - formalize some part of existing mathematics, assuming that there is a system that is easy enough to learn and use to make this feasible. In my view there is a real benefit to really having to understand a proof on this detailed level. 

This makes me think that, if there is a suitable system and an agreed standard, the database of 'standard' mathematics that has been formalized might start to grow rather quickly. Am I being naive?

> Further, libraries implemented in a system based on type theory like 
> Coq or Agda are useless if you use Isabelle or HOL4, systems based on 
> HOL. Even the statements of theorems and techniques used to formalise
> e.g. matrices and linear algebra would need considerable work to port 
> from Coq or Agda to Isabelle due to the vastly different foundations of 
> the two groups of systems.

This to me seems like a much more serious issue. Incompatible languages would seem to not only cause a duplication of efforts, but also may cause people (like myself) to hesitate about investing the time required to use one of these. Is there a serious effort towards achieving a translation between the different systems, or at least building a system in which the current systems can both be interpreted?

---
Sam Sanders critiqued my contention that "that eventually all rigorous mathematical results should routinely come with a formal verification". (Of course, it is dangerous to make such absolute statements...) He also feels that advances in Artificial Intelligence would be necessary for my aim. To avoid unproductive discussions, let me try to isolate a key point.

Let me use "mathematically rigorous" for a proof that is rigorous in the sense it is often taught in undergraduate mathematics, e.g. at the level of detail of an epsilon-delta proof, a completely worked-out proof by induction, etc. 

(Most published mathematical proofs are not written in this style. I believe - again perhaps naively - that, to claim a proof, I should at least be confident that I would be able to produce such a mathematically rigorous proof with a limited amount of extra effort, and without requiring new ideas. However, this is a somewhat separate issue from formal verification.)

My feeling has been that it ought to be feasible to pass from a mathematically rigorous proof to a computer-verifiable one with a modest time commitment (i.e., comparable to that of achieving the mathematically rigorous proof in the first place). It would surprise me if this really required substantial advances in AI, rather than good language and system design in collaboration with working mathematicians. Is there something I am missing?

---
Arnold Neumaier gives a very useful estimate on this final point:

> Making a mathematically fully acceptable proof written in Latex 
> formally rigorous (i.e., acceptable to a proof assistent) has an 
> overhead factor of roughly 40.

He also notes:
> The main obstacle is the lack of mathematician-friendliness of all 
> available software systems, which repels most working mathematicians.

Clearly a factor of 40 is prohibitive. Is it realistic to reduce this drastically (let us say, to a factor of 2 or 3) using current knowledge?
---

Freek Wiedijk also comments on the differences between type theory and HOL systems, and the difficulty in overcoming them (see above).

Regarding engagement from 'mainstream mathematicians', he says:

> It would help if it became clear whether these people consider it 
> important to have full classical ZFC available or not (i.e., whether 
> they don't mind working in the formal world of Bishop's mathematics, 
> where you cannot prove the intermediate value theorem if you state it 
> the naive way, say.)

To this I would answer that it would seem unlikely that many mathematicians (myself included) would want to work in a system where we cannot use the usual version of the intermediate value theorem ... :)

> Currently doing formal proof goes too slowly to be really pleasant.  
> The hammers -- like Isabelle's Sledgehammer -- help, but maybe not 
> enough yet.  You still need to be aware of a lot of details that you 
> normally would leave implicit.
> At least, I think.

Perhaps this is really the key point, and it is hard for me to understand exactly what the overhead is, without getting my hands dirty and actually doing it. Here is a very simple statement which I often give to students as a first exercise in iteration, and to practice formal mathematics.

***
Let f be a real-valued function on the real line, such that f(x)>x for all x. 
Let x_0 be a real number, and define the sequence (x_n) recursively by x_{n+1} := f(x_n). Then x_n diverges to infinity. 
***

A standard proof might go along the following steps: 1) By assumption, the sequence is strictly increasing; 2) hence the sequence either diverges to infinity or has a finite limit; 3) by continuity, any finite limit would have to be a fixed point of f, hence the latter cannot occur.

What effort would be required to formalize this kind of statement using current technology? 

Best wishes,
Lasse