[FOM] Formal verification

[Arnold Neumaier]

On 10/18/2014 10:34 AM, Rempe-Gillen, Lasse wrote:
> I hold the opinion, and have done so since being a graduate student, that eventually all rigorous mathematical results should routinely come with a formal verification.
>
> Key objections raised to my premise in the afore-mentioned discussions were:
> 1) Formal verification would require so much additional effort that progress in mathematics would be effectively hindered by such requirements.
> 2) People currently read some papers to be sure that results being understood are correct. This would cease if they were formally verified, so there would actually be even less reading of papers going on than now.
>
> I see point 1) mainly as a technical point. If you had suggested four decades ago that mathematicians would typeset their own papers, a similar objection may have been made. However, thanks to personal computing and LaTeX, the benefits of doing so now far outweigh the effort. This the standard that verification must achieve in order for its wider use to be viable.

But using Latex has an overhead factor of roughly 2 compared to 
handwriting, which is acceptable in view of the flexibility in 
formatting and modifying it returns to the user, and actually saves time 
if many changes are made over a longer period of time.

Whereas 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, and currently returns nothing but an 
increases assurance of correctness.


> I would be interested to know what, in the view of those who know about the current state of things, is the main current obstacle to a wider use of computer verification in the medium term (say the next 10 years):

Having worked on computer-assisted (as opposed to fully formalized) 
proofs myself, I am closely observing the scene for many years to see 
whether it pays to use formal proof tools, and I still find the ratio 
between quality returned and work to invest appallingly low.

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

Apart from the heavy work needed to feed math precisely enough into a 
theorem prover, both the input and the output are so far away from the 
highly optimized way mathematicians communicate their concepts and 
proofs that the transition from the traditional way to a more formal way 
is made very hard for anyone trying. (Quite unlike Latex.)


 > d) Some fundamental issues on a theoretical level that still need to 
be overcome?

A detailed study of the way the mathematical language communicates a 
host of information between the lines, that currently has to be spelled 
out explicitly for proof systems, would reveal many ways that interfaces 
to theorem provers could exploit to save the mathematician's time. 
Ultimately it would probably even help theorem provers to automatically 
find missing pieces of proofs.


Arnold Neumaier