[FOM] formal proofs (was: Hersh on Flyspeck

[Sam Sanders]

> Perhaps machine proof-checking will finally come of age when an attempt 
> to check an important proof reveals that the informal version of 
> the proof is critically flawed in a way that isn't a mere lack of 
> formality, and places the truth of the theorem in doubt.

Philip Ehrlich has written a paper on the history/development of infinitesimals between the introduction Robinson’s 
Nonstandard Analysis and the notorious false theorem by Cauchy.  It can be found here:

http://www.ohio.edu/people/ehrlich/AHES.pdf

Ehrlich’s well-documented claim is that while certain people (in light of Cauchy’s false theorem) indeed outright banned infinitesimals in favour of Weierstrass’ approach, 
there are others who did the opposite: investigate and develop theories involving infinitesimals (pre-Robinson).  

Ehrlich’s point is that the folklore version of history along the lines of  “After Cauchy’s false theorem everybody renounced infinitesimals"
is incorrect, or at least more complicated than that.

Given history’s tendency to repeat, even if the theorem and critically flawed proof you mention is found, 
this will probably not result in the mathematics community immediately renouncing informal proof (a revolution as it where).  
Rather this will probably start a slower evolution towards more formal proof.   

Best,

Sam