[SystemSafety] Faults in maths proofs

[Derek M Jones]

Les,

> Take the Americans. Having got rid of Trump they’re on their way, giving more credibility to

We will find out who is going to be the next president of the US on
Monday, when the electoral college votes.

Given the obvious volume of fraud in the swing states some states
may decide not to cast their votes.

The news media have been reporting that there has not been widespread fraud,
this is true, it only happened in the swing states.
The news media are also reporting that there has not been any organized vote
rigging.  The 'unusual' pattern of voting is better explained by lots of
individuals independently 'doing their bit' to add in some votes in the
swing states.

Next week could be very surprising to many people, or it could be dull.

> Les
> 
>> 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.
>>>
> 
> 
> 
> --
> Les Chambers
> les at chambers.com.au
> +61 (0)412 648 992
> 
> 
> _______________________________________________
> The System Safety Mailing List
> systemsafety at TechFak.Uni-Bielefeld.DE
> Manage your subscription: https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety
> 

-- 
Derek M. Jones           Evidence-based software engineering
tel: +44 (0)1252 520667  blog:shape-of-code.coding-guidelines.com