[SystemSafety] Faults in maths proofs

Olwen Morgan olwen at phaedsys.com
Fri Dec 11 16:32:39 CET 2020

Another gem of scepticism from Derek. This time he is due unambiguous 
thanks. (There's condescension for you!)

Yet one does not need to turn to complex mathematics to find examples of 
potentially perfidious proofs.

Consider the equation: ax^3 e^-x = 1.

With only a little wrangling, it is easy to *see* that this equation has 
exactly one root when a = (e/3)^3 . Now, according to Galculator, this 
quantity is approximately equal to 0.743908774934. Hence one *expects* 
that the equation

0.74391x^3 e^-x has exactly two real roots very close together - as can 
be found by numerical solution using Newton's method. ... But the 
question now arises as to *what would constitute a rigorous proof* that 
this equation has exactly two real roots?

I'll leave this as a teaser for the more mathematically literate on this 


On 10/12/2020 15:54, Derek M Jones wrote:
> All,
> "What is Mathematics?"
> https://www.andrew.cmu.edu/user/avigad/meetings/fomm2020/slides/fomm_buzzard.pdf 
> A discussion involving recent examples of 'proofs'
> that may or may not be correct, starting at slide 5.
> There is some discussion of the use of programs to create proofs,
> and the problem that software contains faults, just like mathematical 
> proofs.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/pipermail/systemsafety/attachments/20201211/59e0513f/attachment.html>

More information about the systemsafety mailing list