[SystemSafety] Faults in maths proofs

[Olwen Morgan]

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


Olwen




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>