# Canal-U

Mon compte

## Proofs assistants : from symbolic logic to real mathematics

Copier le code pour partager la vidéo :
<div style="position:relative;padding-bottom:56.25%;padding-top:10px;height:0;overflow:hidden;"><iframe src="https://www.canal-u.tv/video/inria/embed.1/proofs_assistants_from_symbolic_logic_to_real_mathematics.35491?width=100%&amp;height=100%" style="position:absolute;top:0;left:0;width:100%;height: 100%;" width="550" height="306" frameborder="0" allowfullscreen scrolling="no"></iframe></div> Si vous souhaitez partager une séquence, indiquez le début de celle-ci , et copiez le code : h m s
Auteur(s) :
Paulson Lawrence

Producteur Canal-U :
Inria
Contacter la chaine
J’aime
Imprimer
partager

### Proofs assistants : 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 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

•
•
Date de réalisation : 18 Mai 2017
Durée du programme : 63 min
Classification Dewey : Mathematical logic (Symbolic logic)
•
Catégorie : Conférences
Niveau : niveau Master (LMD), niveau Doctorat (LMD), Recherche
Disciplines : Mathématiques, Informatique
Collections : Colloquium Jacques Morgenstern : recherches en STIC - nouveaux thèmes scientifiques, nouveaux domaines d’application, et enjeux
ficheLom : Voir la fiche LOM
•
Auteur(s) : Paulson Lawrence
Editeur : INRIA (Institut national de recherche en informatique et automatique) , CNRS - Centre National de la Recherche Scientifique , UNS
•
Langue : Anglais
Mots-clés : preuve de programme

## commentaires

Ajouter un commentaire Lire les commentaires
*Les champs suivis d’un astérisque sont obligatoires.
Aucun commentaire sur cette vidéo pour le moment (les commentaires font l’objet d’une modération)