[FOM] Formal verification

[Rempe-Gillen, Lasse]

The current discussion concerning formal verification of proofs is very interesting to me. 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.

The benefits of this do not seem to be universally accepted within mathematics. In fact, I recently had a discussion with two excellent junior mathematicians, both of whom were highly sceptical regarding the concept. This indicates that the above is not - as I may have naively thought as a graduate student - an inevitable development, but rather might require substantial effort, or perhaps a catalytic event such as an area collapsing as a result of errors being discovered in previous work.

(The likelihood of the latter still appears slim. However, there are plenty of examples of serious results where significant gaps were later discovered and had to be filled, which in itself may erode the concept of mathematics as an absolutely rigorous discipline.)

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.

Point 2) is a valid point, but not in my view significant enough to outweigh the benefits of verification to the discipline.

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):

a) Competing systems and paradigms in the formal proof community;
b) Lack of engagement from 'mainstream' research mathematicians;
c) Lack of funding;
d) Some fundamental issues on a theoretical level that still need to be overcome?

Best wishes,
Lasse

PS. Some years ago I actually tried to contact people in the Mizar community to try and find out what it would take to verify some of my own results with more elementary proofs. However, I never received a response, and found the documentation available rather impenetrable. I was also put off by the impression that it was not possible to run Mizar "conditionally", i.e. formalize the statements of some standard results and verify a proof subject to their correctness - which is inevitably going to be necessary in the initial stages if verification is to be brought into wider mathematics.

--------------------------------------------------------------
Prof. Lasse Rempe-Gillen
Deputy Head of Department for REF
Dept. of Math. Sciences, Univ. of Liverpool, Liverpool L69 7ZL
Office 520; tel. +44 (0)151 794 4025, fax +44 (0)151 794 4061
http://pcwww.liv.ac.uk/~lrempe
--------------------------------------------------------------

-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20141018/22a7a8b7/attachment.html>