[SystemSafety] Logical difficulties in mathematics
Peter Bernard Ladkin
ladkin at causalis.com
Sun Feb 24 07:42:51 CET 2019
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
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
Prof. Peter Bernard Ladkin, Bielefeld, Germany
Je suis Charlie
Tel+msg +49 (0)521 880 7319 www.rvs-bi.de
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 833 bytes
Desc: OpenPGP digital signature
More information about the systemsafety