[SystemSafety] Number Theorist Fears All Published Math Is Wrong

[Peter Bernard Ladkin]

On 2019-10-29 13:44 , Derek M Jones wrote:
> 
> ... size and complexity leads people to suspect
> that much of [modern mathematics] contains faults:
> https://www.vice.com/en_us/article/8xwm54/number-theorist-fears-all-published-math-is-wrong-actually
> 
> The solution being proposed?
> Use software to help check the mathematical proofs.
First, recall the story I have shared here (twice? more?) about Leslie Lamport's talk from 30 years
ago on rigor and faults in published mathematics.

Second, there are a number of ongoing projects in math-proving. The Isabelle team have an archive of
formal proofs at https://www.isa-afp.org . In a piece of well-regarded work, Georges Gonthier proved
the Four-Color Theorem using Coq. One of my last students in Bielefeld was very interested in
mathematics using ATP technology, Coq in particular, and now is working on a PhD in Erlangen with
Michael Kohlhase using another system (he was working on the Math library of Bill Farmer's IMPS
prover, but I am not sure quite what his topic is now).

PBL

Prof. Peter Bernard Ladkin, Bielefeld, Germany
MoreInCommon
Je suis Charlie
Tel+msg +49 (0)521 880 7319  www.rvs-bi.de





-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20191029/5ab70ce9/attachment.sig>