[FOM] Formal verification
Arnold.Neumaier at univie.ac.at
Tue Oct 21 08:33:47 EDT 2014
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
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.
More information about the FOM