[FOM] formal proofs (was: Hersh on Flyspeck

[katzmik at macs.biu.ac.il]

Robinson was the first to challenge the idea that Cauchy's sum theorem was
"critically flawed".  Detlef Laugwitz (of Schmieden-Laugwitz fame) developed
these ideas in detail.  It emerges that the error can only be attributed to
Cauchy if we assume that he was working with the real Archimedean continuum
that we (as well as modern historians of mathematics) are accustomed to.  If
one drops this assumption, Cauchy's statement can be interpreted as correct. 
Here Laugwitz interprets the hypothesis of Cauchy's theorem as requiring
convergence at what today would be called nonstandard points in addition to
the real points.  Then one does get a correct theorem.  My own position,
unlike Laugwitz's, is that the exact hypothesis Cauchy may have had in mind in
1821 is too ambiguous to decide.  Meanwhile in an 1853 article Cauchy
specifically extended the hypothesis to include additional points. This is
dealt with in an article by Borovik and myself here:
http://dx.doi.org/10.1007/s10699-011-9235-x
MK


On Sun, October 12, 2014 15:06, Sam Sanders wrote:
>
>> 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
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>