Il y a 4 Résultats avec le mot clé : "laboratoire commun Inria - Microsoft Research"
© Bernard Lachaud
Preuve informatique
La précision des ordinateurs au service des mathématiques
Avec l’équipe Typical d’Inria Saclay - Ile-de-France, l’équipe Marelle de Sophia Antipolis a largement participé à l’aventure du projet Mathematical Components , sous la houlette de Georges Gonthier, dans le cadre du laboratoire commun Inria Microsoft Research.
Retour sur une expérience passionnante avec l’une des chercheuses de Marelle, Laurence Rideau.
Mots-clés :
- Mathematical components
- Equipe-projet MARELLE
- Coq
- Laboratoire commun Inria - Microsoft Research
- Inria research centre - Sophia Antipolis - Méditerranée
Accueil > Centre > Saclay > Actualités > La précision des ordinateurs au service des mathématiques
© Photo Bernard Lachaud
Preuve informatique
La preuve mathématique par informatique !
Une démonstration formelle complète, certifiée par le logiciel Coq, a été annoncée en septembre par Georges Gonthier et son équipe du laboratoire commun Inria-Microsoft Research.
Ces travaux rendent artificielle l’opposition entre informatique et mathématiques, le dénominateur commun étant la logique. Parmi les "compagnons de route" de Georges Gonthier, deux jeunes chercheurs se réjouissent d’avoir participé à l’aventure et "grandi" avec le projet Mathematical Components (MathComp). Témoignages…
Mots-clés :
- Preuve
- Georges Gonthier
- Inria Sophia Antipolis - Méditerranée
- Inria Saclay - Île-de-France
- Enrico Tassi
- Assia Mahboubi
- Laboratoire commun Inria - Microsoft Research
- Théorème Feit et Thompson
Accueil > Recherches > Actualités > La preuve mathématique par informatique !
© Laboratoire commun Inria-Microsoft Research
Preuve informatique
Georges Gonthier : Notre diagramme de travail ressemblait à un plan de guerre napoléonienne !
Six années se sont écoulées entre le début du projet et la fin de la preuve du théorème de Feit et Thompson réalisée le 20 septembre 2012. Récit d’une aventure moderne.
Entretien avec Georges Gonthier, laboratoire commun Microsoft Research-Inria.
Mots-clés :
- Inria Saclay - Île-de-France
- Théorème Feit et Thompson
- Inria Sophia Antipolis - Méditerranée
- Georges Gonthier
- Preuve
- Laboratoire commun Inria - Microsoft Research
Accueil > Recherches > Actualités > Georges Gonthier : Notre diagramme de travail ressemblait à un plan de guerre napoléonienne !
© Inria / Photo Kaksonen
Preuve informatique
Un grand succès pour la preuve informatique
Six ans après la démonstration par ordinateur du théorème des quatre couleurs, Georges Gonthier et son équipe réussissent la démonstration, autrement plus complexe, du théorème de Feit et Thompson, un théorème central pour la théorie des groupes et leur classification. Grand pas pour les mathématiques, qui s’appuient de plus en plus sur la preuve par ordinateur, c’est surtout une réussite pour l’informatique qui montre là sa capacité à déployer des outils et des techniques de qualité pour codifier les mathématiques.
Mots-clés :
- Inria Saclay - Île-de-France
- Georges Gonthier
- Preuve
- Laboratoire commun Inria - Microsoft Research
- Théorème Feit et Thompson
- Inria Sophia Antipolis - Méditerranée
Accueil > Recherches > Actualités > Un grand succès pour la preuve informatique
Centres de recherche Inria
- Sophia (4)
