Ressource en auto-formation : From symbolic logic to real mathematics

Mathematicians have always been prone to error. As proofs get longer and more complicated, the question of correctness looms ever larger. Andrew Wiles’ proof of Fermat’s last theorem contained a flaw that was only fixed a year later. Meanwhile, proof assistants — formal tools originally develope...
cours / présentation - Création : 18-05-2017
Par : Lawrence Paulson
Partagez !

Présentation de: From symbolic logic to real mathematics

Informations pratiques sur cette ressource

Langue du document : Anglais
Type : cours / présentation
Niveau : master, doctorat
Durée d'exécution : 1 heure 2 minutes 37 secondes
Contenu : vidéo
Document : video/mp4
Poids : 1.10 Go
Droits d'auteur : libre de droits, gratuit
Droits réservés à l'éditeur et aux auteurs.

Description de la ressource en auto-formation

Résumé

Mathematicians have always been prone to error. As proofs get longer and more complicated, the question of correctness looms ever larger. Andrew Wiles’ proof of Fermat’s last theorem contained a flaw that was only fixed a year later. Meanwhile, proof assistants — formal tools originally developed in order to verify hardware and software — are growing in sophistication and are being applied more and more to mathematics itself. When will proof assistants finally become useful to working mathematicians? Mathematicians have used computers in the past, for example in the 1976 proof of the four colour theorem, and through computer algebra systems such as Mathematica. However, many mathematicians regard such proofs as suspect. Proof assistants (e.g. Coq, HOL and Isabelle/HOL) are implementations of symbolic logic and were originally primitive, covering only tiny fragments of mathematical knowledge. But over the decades, they have grown in capability, and in 2005, Gonthier used Coq to create a completely formal proof of the four colour theorem. More recently, substantial bodies of mathematics have been formalised. But there are few signs of mathematicians adopting this technology in their research.   Today’s proof assistants offer expressive formalisms and impressive automation, with growing libraries of mathematical knowledge. More however must be done to make them useful to mathematicians. Formal proofs need to be legible with a clear connection to the underlying mathematical ideas. Natural language must play a stronger role, and our millions of lines of existing proofs surely contain hints to aid in the construction of new proofs

"Domaine(s)" et indice(s) Dewey

  • Mathematical logic (Symbolic logic) (511.3)

Domaine(s)

Intervenants, édition et diffusion

Intervenants

Fournisseur(s) de contenus : INRIA (Institut national de recherche en informatique et automatique), CNRS - Centre National de la Recherche Scientifique, UNS

Diffusion

Document(s) annexe(s) - From symbolic logic to real mathematics

Partagez !

AUTEUR(S)

  • Lawrence Paulson

DIFFUSION

Cette ressource en auto-formation vous est proposée par :
Canal-U - accédez au site internet
Sur les réseaux sociaux :

EN SAVOIR PLUS

  • Identifiant de la fiche
    35491
  • Identifiant OAI-PMH
    oai:canal-u.fr:35491
  • Schéma de la métadonnée
  • Entrepôt d'origine
    Canal-U

Ressources en auto-formation sur les mêmes thèmes

Présentation de la ressource en auto-formation Approches fonctionnelles de la programmation cours / présentation
23/02/2009
Approches fonctionnelles de la programmation
Auteur(s) : Verna Didier
Description : Fournir un panorama complet du paradigme de programmation fonctionnelle et de son positionnement par rapport aux autres paradigmes de programmation (en particulier de la programmation impérative). Illustrer l'ensemble des concepts abordés au moyen de deux langages fonctionnels: Lisp et Haskell.
Présentation de la ressource en auto-formation Du rêve à la réalité des preuves cours / présentation, démonstration
08/06/2012
Du rêve à la réalité des preuves
Auteur(s) : Delahaye Jean-Paul
Description : Les ordinateurs ne savent pas prouver seuls des théorèmes profonds. Cependant, grâce aux assistants de preuve, ils garantissent les démonstrations découvertes par les mathématiciens.