[SystemSafety] Logical difficulties in mathematics

[Peter Bernard Ladkin]

On 2019-02-15 21:09 , David MENTRÉ wrote:
> 
> For more "classical" use of formal methods in Mathematics, you can look
> at Gonthier et al. proof of 4 colours theorem ... or .....
> proof of Feit-Thompson Odd Order Theorem ... Beyond the
> demonstration of those theorems, those works built a huge work of
> formalized Mathematics in a mechanized way using Coq proof assistant
> (https://github.com/math-comp/math-comp).
There is also the substantial work on formal proofs in mathematics using the Cambridge-München
Isabelle prover. There is an archive of formal proofs at https://www.isa-afp.org and the Isabelle
home page is at https://isabelle.in.tum.de/index.html (one of four mirrored sites).

I don't know much about Homotopy Type Theory, but Georges Gonthier was also involved in that, along
with other luminaries such as the logicians Peter Aczel, Per Martin-Löf and Dana Scott
https://hal.inria.fr/hal-00935057

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/20190224/3b01a3bb/attachment.sig>