Aujourd’hui quand quelqu’un annonce un nouveau résultat mathématique, il peut être très difficile de savoir si le résultat est correct ou non ; il sera peut-être un jour réaliste de demander à la personne de fournir une preuve vérifiée par un assistant de preuve, pour accélérer son étude et sa compréhension par les scientifiques du domaine.
Je ne comprends pas du tout cette phrase.
Actuellement quand un résultat de math est démontré par un chercheur (la preuve du dernier théorème de Fermat par Wiles par exemple) alors le chercheur écrit un article à destination de ses collègues pour expliquer sa démonstration.
Les collègues lisent l'article, évaluent la rigueur et la pertinence des arguments et finalement portent un jugement sur la véracité de la démonstration.
Ce qu'il faut bien voir c'est que l'auteur écrit son article pour optimiser la compréhension auprès de ses collègues. Ce sont eux (les pairs) qui vont évaluer son travail.
L'article n'est pas écrit dans un langage formel évaluable par une machine. Il est écrit avec des phrases et des mots.
Certains points, considérés comme de la routine pour les spécialistes du domaine, sont abrégés ou carrément passés sous silence.
Par exemple dans de nombreux articles de géométrie arithmétique ou de géométrie algébrique on peut voir des phrases du style : "Par un argument à la GAGA il est facile de voir que blabla".
Les spécialistes comprennent immédiatement que cela fait référence à l'article ultra-connu de Jean-Pierre Serre intitulé "Géométrie algébrique et géométrie analytique".
Mais une machine ne comprendrait pas ça. Pour une machine tout doit être complètement formalisé.
Donc tout ça pour dire que ta phrase affirmant qu'une démonstration "vérifiée par un assistant de preuve accélérait son étude et sa compréhension par les scientifiques du domaine" ne tient pas debout. Cette preuve serait au contraire illisible par un humain si on la compare aux articles actuels qui, eux, sont écrits pour des humains.
La vérification formelle des démonstrations pourra sans doute être très utile pour avoir la certitude qu'il n'y a pas d'erreurs qui se sont glissés dans le raisonnement. C'était le pari de Voevodsky.
Mais il y a très peu de chance pour que, en soi, cela favorise la compréhension.
# Math
Posté par patrick_g (site web personnel) . En réponse au journal La recherche en langages de programmation au quotidien. Évalué à 8. Dernière modification le 17 mai 2018 à 09:13.
Je ne comprends pas du tout cette phrase.
Actuellement quand un résultat de math est démontré par un chercheur (la preuve du dernier théorème de Fermat par Wiles par exemple) alors le chercheur écrit un article à destination de ses collègues pour expliquer sa démonstration.
Les collègues lisent l'article, évaluent la rigueur et la pertinence des arguments et finalement portent un jugement sur la véracité de la démonstration.
Ce qu'il faut bien voir c'est que l'auteur écrit son article pour optimiser la compréhension auprès de ses collègues. Ce sont eux (les pairs) qui vont évaluer son travail.
L'article n'est pas écrit dans un langage formel évaluable par une machine. Il est écrit avec des phrases et des mots.
Certains points, considérés comme de la routine pour les spécialistes du domaine, sont abrégés ou carrément passés sous silence.
Par exemple dans de nombreux articles de géométrie arithmétique ou de géométrie algébrique on peut voir des phrases du style : "Par un argument à la GAGA il est facile de voir que blabla".
Les spécialistes comprennent immédiatement que cela fait référence à l'article ultra-connu de Jean-Pierre Serre intitulé "Géométrie algébrique et géométrie analytique".
Mais une machine ne comprendrait pas ça. Pour une machine tout doit être complètement formalisé.
Donc tout ça pour dire que ta phrase affirmant qu'une démonstration "vérifiée par un assistant de preuve accélérait son étude et sa compréhension par les scientifiques du domaine" ne tient pas debout. Cette preuve serait au contraire illisible par un humain si on la compare aux articles actuels qui, eux, sont écrits pour des humains.
La vérification formelle des démonstrations pourra sans doute être très utile pour avoir la certitude qu'il n'y a pas d'erreurs qui se sont glissés dans le raisonnement. C'était le pari de Voevodsky.
Mais il y a très peu de chance pour que, en soi, cela favorise la compréhension.