7 décembre 2013

13 messages - Retourner à l'article
  • À la croisée des fondements des mathématiques, de l’informatique et de la topologie

    le 7 décembre 2013 à 16:12, par François Loeser

    Une coquille semble-t-il : au lieu de « Le formalisme de la théorie des types constitue une alternative à la théorie des types » il faut lire « Le formalisme de la théorie des types constitue une alternative à la théorie des ensembles »

    Répondre à ce message
    • Une coquille...

      le 7 décembre 2013 à 21:56, par Antoine Chambert-Loir

      Bien entendu, c’était une coquille... j’en suis désolé !

      Répondre à ce message
  • À la croisée des fondements des mathématiques, de l’informatique et de la topologie

    le 7 décembre 2013 à 16:21, par Julien Puydt

    Si je puis me permettre : « Le formalisme de la théorie des types constitue une alternative à la théorie des types pour décrire les fondements des mathématiques. » devrait plutôt être : « Le formalisme de la théorie des types constitue une alternative à la théorie des ensembles pour décrire les fondements des mathématiques. »

    Répondre à ce message
    • À la croisée des fondements des mathématiques, de l’informatique et de la topologie

      le 7 décembre 2013 à 21:56, par Antoine Chambert-Loir

      Oui, merci !

      Répondre à ce message
  • À la croisée des fondements des mathématiques, de l’informatique et de la topologie

    le 9 décembre 2013 à 13:32, par Pierre Lecomte

    Merci d’avoir attiré l’attention sur ce livre, par votre bel et clair article !

    Répondre à ce message
  • À la croisée des fondements des mathématiques, de l’informatique et de la topologie

    le 9 décembre 2013 à 15:18, par Claude Animo

    Une remarque concernant les preuves automatiques et votre commentaire louangeur concernant « des logiciels de vérification de preuve, tels que Coq (initialement issu du Calculus of Constructions de Thierry Coquand) qui ont récemment eu de jolis succès en permettant la vérification par Georges Gonthier et son équipe du théorème des 4 couleurs ou du théorème de Feit-Thompson » :

    . combien de pages pour ces démonstration ?

    . sont-elles lisibles ? combien de millions d’inférences ?

    . qui peut les relire.

    . qui a démontré le démonstrateur ? lui-même ? un autre ?

    En conclusion, peut-on encore parler de démonstrations donc de preuves ?

    Répondre à ce message
  • À la croisée des fondements des mathématiques, de l’informatique et de la topologie

    le 10 décembre 2013 à 00:08, par Antoine Chambert-Loir

    Je n’ai pas regardé les vérifications de l’équipe de Gonthier, mais j’avais jeté un œil au livre de Thomas Hales (Dense sphere packings — A blueprint for formal proofs), qui est assez lisible (c’est, si je puis dire, une traduction en langage usuel de la preuve formelle). De fait, ainsi qu’explique Hales (par exemple dans son article « Mathematics in the Age of the Turing Machine »), les preuves formalisées ne sont guère plus longues que les preuves originelles.)

    Enfin, les logiciels de vérifications de preuves ont un noyau initial très petit qu’on peut vérifier facilement, et le reste est fait de proche en proche (un peu comme les compilateurs des langages modernes).

    Enfin, entre des dizaines de pages d’études de cas, et une description formelle des calculs qu’il faut mener, jointe au résultat de leur vérification mécanisée, je vous laisse juge de ce qui est le plus sûr.

    Toutefois, vérifier informatiquement une preuve n’améliore a priori pas la compréhension des mathématiques (à moins que pour ne faire cette vérification, on n’ait été amené à penser différemment la preuve que l’on vérifie). Cette dernière assertion doit être bémolisée : dans le livre dont cette chronique est l’objet, de nombreuses preuves ont d’abord été menées à l’aide du logiciel de vérification de preuve (qui mérite dans ce cas son nom d’« assistant de preuves »).

    Répondre à ce message
    • À la croisée des fondements des mathématiques, de l’informatique et de la topologie

      le 10 décembre 2013 à 13:45, par Claude Animo

      « Toutefois, vérifier informatiquement une preuve n’améliore a priori pas la compréhension des mathématiques (à moins que pour ne faire cette vérification, on n’ait été amené à penser différemment la preuve que l’on vérifie). »

      Dès lors qu’une démonstration automatique échoue à se terminer (critère subjectif), il est possible d’affirmer, après s’être imprégné du déroulé partiel de la preuve, que son aboutissement nécessitera une meilleure compréhension des mathématiques mises en jeu (création de nouveaux objets et structures ?) pour parvenir à casser (divide and conquer) la complexité irréductible du processus en utilisant un autre schéma de démonstration (démontrer par exemple le lemme ad hoc au moment opportun).

      C’est en dessinant en creux nos difficultés à aboutir, que la preuve automatique, peut, me semble-t-il, éventuellement s’avérer utile.

      J’ajouterais enfin que le travail le plus important consiste à « axiomatiser » la preuve et ce travail accompli, on constatera souvent que la démonstration est alors pratiquement réalisée (j’exagère un peu).

      Merci en tout cas pour ce « hors piste » roboratif et plein d’énergie.

      Répondre à ce message
      • À la croisée des fondements des mathématiques, de l’informatique et de la topologie

        le 17 décembre 2013 à 10:53, par Jérôme Germoni

        Attention, il n’est pas question de « preuve automatique » dans toutes ces affaires mais de « preuve formelle ». L’assistant de preuve ne produit pas une preuve à partir de rien : il certifie la validité d’une preuve qui a déjà été produite (par un humain) et qui est traduite (par un humain) dans un langage qu’il comprend. Une preuve formelle est composée d’une part de la traduction d’une preuve (qui devient un objet mathématique à part entière grâce à la théorie des types et pas un discours humain) et d’autre part d’un certificat de ladite preuve.

        Répondre à ce message
  • À la croisée des fondements des mathématiques, de l’informatique et de la topologie

    le 11 décembre 2013 à 17:46, par électron

    On peut signaler aussi que la théorie des catégories, qui est très générique, trouve des applications dans d’autres domaines tels que la linguistique (grammaires catégorielles) et la physique. Un formalisme simple permet déjà d’effectuer des traitements sophistiqués.

    Olivier

    Répondre à ce message
  • À la croisée des fondements des mathématiques, de l’informatique et de la topologie

    le 21 décembre 2013 à 21:19, par Anthony Bordg

    Merci à Antoine Chambert-Loir pour cette très bonne introduction. Je me permets d’ajouter pour répondre à certaines inquiétudes que l’avantage de la théorie des types et en particulier de la théorie des types avec l’axiome d’univalence est qu’elle permet des preuves formelles qui sont de tailles tout à fait comparables aux preuves informelles (évidemment des preuves informelles comme dans la pratique courante des mathématiciens sont aussi possibles, c’est d’ailleurs le choix de présentation du livre mentionné) et qui restent relativement compréhensibles. Evidemment rien n’interdit en théorie des ensembles, disons ZFC, des preuves formelles mais celles-ci deviennent vite incompréhensibles même aux mathématiciens chevronnés et sont d’une complexité qui explose très vite. Cette mise au pas de la formalisation et l’absence d’énoncés
    sans sens sont donc deux avantages des fondations univalentes qui ressortent bien de l’article de monsieur Chambert-Loir.

    Répondre à ce message
    • À la croisée des fondements des mathématiques, de l’informatique et de la topologie

      le 26 mai 2016 à 21:24, par Boule Chevelue

      Bonjour,

      Quand vous dites : « l’avantage de la théorie des types et en particulier de la théorie des types avec l’axiome d’univalence est qu’elle permet des preuves formelles qui sont de tailles tout à fait comparables aux preuves informelles » et : « Evidemment rien n’interdit en théorie des ensembles, disons ZFC, des preuves formelles mais celles-ci deviennent vite incompréhensibles même aux mathématiciens chevronnés et sont d’une complexité qui explose très vite », s’agit-il d’observations empiriques ou existe-il des résultats précis sur les complexités de ces différentes preuves ?

      Répondre à ce message
  • À la croisée des fondements des mathématiques, de l’informatique et de la topologie

    le 16 avril 2014 à 09:40, par Jérôme Germoni

    Le séminaire Bourbaki de juin 2014 met la théorie homotopique des types et la preuve formelle au programme : un exposé de Thierry Coquand sur Théorie des types dépendants et axiome d’univalence et un de Thomas Hales sur Developments in formal proofs.

    Répondre à ce message
Pour participer à la discussion merci de vous identifier : Si vous n'avez pas d'identifiant, vous pouvez vous inscrire.