[FOM] Formal verification

[Sam Sanders]

> 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.

One could similarly say that “all rigorous results in physics should routinely come with a rigorous mathematical backbone”, where mathematical rigour is understood as the current standard in mathematics.  
However, enforcing such rigour onto physics would bring the latter to a grinding halt (in my opinion).  Informal mathematics allows physicist to concentrate on the physics of the problem.  One could argue
that some level of informal math is therefore essential to physics.  (I am talking physics general, not just theoretical physics).  

By analogy, enforcing formal verification onto math would impede the latter’s development.  (Unless one simply redefines math as “formalized math”, but that is cheating in my book)  

> 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.
> 
> 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.

The problem with the often-heard analogy between LaTeX and formal verification is the following:

Many people nowadays (say younger than 35-40) grew up with computers and had some experience 
using them (Word, games, internet, perhaps some programming…) before they were exposed to LaTeX.  They did not have to 
start from scratch:  LaTeX was just another part of personal computing for many.  This substantially lowers the learning curve.  

There is no analogue for formal verification: Even very few mathematicians have ever encountered anything remotely
like the level of ‘formalility' in formal verification.  There is no prior experience and the learning curve is therefore quite steep.  

The above need not be the case forever: If AI becomes part of our everyday lives (as it might in the future), and people “grow up with it”, 
then it will be normal that AI does formalization for us mathematicians, and we can achieve the standard you talk about:  (but that is still a big leading “IF”)

> This the standard that verification must achieve in order for its wider use to be viable.

Agreed. 

Best,

Sam Sanders