Prouver à l'aide de l'infini / Philippe Pajot

Article

Pajot, Philippe

En démontrant un théorème de logique mathématique, une informaticienne a fait le pont entre théorie de la démonstration et logique infinitaire. De plus, cette preuve est constructive, ce qui autorise, en principe, une implémentation dans un ordinateur.

Voir le numéro de la revue «La Recherche, 534, Avr. 2018»

Autres articles du numéro «La Recherche»

Suggestions

Du même auteur

Théorème de théorie des groupes vérifié par ordinateur (Un) / Philippe Pajot | Pajot, Philippe

Théorème de théorie des groupes vérifié par o...

Article | SYRACUSE | Pajot, Philippe | 2013

En codant de nombreuses théories d'algèbre, des informaticiens sont parvenus à vérifier par ordinateur la démonstration d'un important théorème de théorie des groupes. Ce succès ouvre la voie à la vérification de problèmes mathéma...

Comment vibrent les espaces abstraits issus de l'arithmétique ? / Philippe Pajot | Pajot, Philippe

Comment vibrent les espaces abstraits issus d...

Article | SYRACUSE | Pajot, Philippe | 2013

Mettant à profit les nouveaux liens qui se tissent entre géométrie et arithmétique, une équipe française a démontré une conjecture datant de 1992 sur la manière dont vibrent certains espaces géométriques abstraits issus de la théo...

L' Estimation du nombre de points rationnels sur des surfaces / Philippe Pajot | Pajot, Philippe

L' Estimation du nombre de points rationnels ...

Article | SYRACUSE | Pajot, Philippe | 2013

Arithmétique et géométrie sont intimement liées dans les travaux visant à compter les points à coordonnées rationnelles sur des surfaces. Une conjecture pour une famille de surface vient d'être résolue.

Géométrie sur des ensembles de points isolés / Philippe Pajot | Pajot, Philippe

Géométrie sur des ensembles de points isolés ...

Article | SYRACUSE | Pajot, Philippe | 2013

Comment étudier des ensembles de points où tout est identique à une partie ? A l'aide d'une fonction particulière. Driss Essouabri nous livre les fondements d'une nouvelle théorie qui vise à comprendre la géométrie de ces ensemble...

Hervé This ou les saveurs atomisées / Philippe Pajot | Pajot, Philippe

Hervé This ou les saveurs atomisées / Philipp...

Article | SYRACUSE | Pajot, Philippe | 2013

Manger des aliments ? Dépassé ! Pionnier de la cuisine moléculaire, le chimiste concocte désormais les recettes du futur avec des composés purs.

Coq. Les maths ont trouvé leur maître / Philippe Pajot | Pajot, Philippe

Coq. Les maths ont trouvé leur maître / Phili...

Article | SYRACUSE | Pajot, Philippe | 2013

Pour qu'un théorème soit juste, il faut qu'il soit démontré. Ce qui nécessite des dizaines et des dizaines de pages de raisonnement... qu'un logiciel, baptisé Coq, permet aujourd'hui de vérifier automatiquement et, surtout, de val...

Du même sujet

Le Vivant, plus fort que l'électronique / Jean-Paul Delahaye | Delahaye, Jean-Paul

Le Vivant, plus fort que l'électronique / Jea...

Article | SYRACUSE | Delahaye, Jean-Paul | 2017

Des systèmes biologiques sont capables d'enregistrer de l'information et de la manipuler, comme le font les ordinateurs. Fondées sur ce constat, de nouvelles technologies informatiques pourraient concurrencer celles d'aujourd'hui....

Algorithmes d'apprentissage pour mieux classifier (Des) / Corinna Cortes | Cortes, Corinna

Algorithmes d'apprentissage pour mieux classi...

Article | SYRACUSE | Cortes, Corinna | 2009

Classer des documents, des phrases orales, des séquences moléculaires, etc. : tel est l'un des défis actuels de l'informatique. Les chercheurs mettent au point de nouvelles méthodes, plus générales et plus efficaces.

Gérard Berry, chercheur en informatique : Pédagogue du numérique / Azar Khalatbari | Khalatbari, Azar (1961-2022)

Gérard Berry, chercheur en informatique : Péd...

Article | SYRACUSE | Khalatbari, Azar (1961-2022) | 2015

Ce pionnier de la programmation, médaille d'or 2014 du CNRS, milite pour une meilleure reconnaissance de sa discipline.

Et les ordinateurs devinrent organiques / Charlotte Mauger | Mauger, Charlotte

Et les ordinateurs devinrent organiques / Cha...

Article | SYRACUSE | Mauger, Charlotte | 2024

En termes d'efficacité énergétique, le cerveau humain continue de supplanter les supercalculateurs. Un constat qui a incité une équipe américaine à intégrer des amas cellulaires à un ordinateur. Et ça marche !

"J'ai mis au point l'ordinateur imprécis" / Vincent Nouyrigat | Nouyrigat, Vincent

"J'ai mis au point l'ordinateur imprécis" / V...

Article | SYRACUSE | Nouyrigat, Vincent | 2012

Autoriser quelques erreurs dans les calculs des processeurs permettrait de gagner en autonomie. Car la course à la précision dont font l'objet depuis cinquante ans les puces informatiques s'avère superflue pour nombre d'applicatio...

Mémordinateurs : quand l'informatique s'inspire du cerveau / Massimiliano Di Ventra | Di Ventra, Massimiliano

Mémordinateurs : quand l'informatique s'inspi...

Article | SYRACUSE | Di Ventra, Massimiliano | 2015

Un peu comme les neurones, de nouveaux composants électroniques traitent l'information et la stockent eux-mêmes. Ils ouvrent la voie à une informatique plus efficace et plus rapide.

Chargement des enrichissements...