[FOM] Formal verification

[Hendrik Boom]

On Tue, Oct 21, 2014 at 09:31:46PM +0000, Rempe-Gillen, Lasse wrote:
> 
> 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? 

At the very least, the effort it takes to assume that f is continuous.

How much effort would be required to express this proof in detail 
based, say, on the background in Landau's Grundlage der Analyse?

Because that book was formalised ages ago in deBruin's Automath system.
I believe it is one of the first hefty theories to be formalized.
The translation of that succinct book became several largish volumes of 
formalism.

Automath was written in Algol 60.  I hear that the system, and the 
translation of Grundlagen, have since been updated to work on midern 
systems.

-- hendrik