Les mathématiciens face au défi des machines

Fin de partie

les mathématiciens face au défi des machines (article du magazine Pour la science,535,mai 2022).

L'article n'est pas en accès libre.

Foys

L'élaboration semi-automatique de la preuve d'un théorème et sa vérification exclusivement par des machines n'est pas nouvelle. Il y a eu le théorème des 4 couleurs démontré en COQ avant.

Fin de partie

@Foys: le théorème des 4 couleurs est évoqué dans l'article en question ainsi que d'autres trucs moins connus du grand public. L'article est intéressant, c'est de la vulgarisation mais il y a beaucoup d'exemples.

Dom

Question naïve : je comprends que l’on établisse qu’un programme (un script ?) est fiable. Par contre comment s’assurer de la fiabilité de « la machine » ?

Fin de partie

@Dom: Comment s'assurer que lorsque tu laisses choir une pièce de monnaie celle-ci va tomber par terre et pas s'envoler vers les cieux?

Dom

Houlala… 🙄
Un seul exemple : https://fr.m.wikipedia.org/wiki/Bug_de_la_division_du_Pentium

Fin de partie

Les sciences physiques sont basées, en particulier, sur la reproductibilité de l'expérience. Dans des conditions données on obtient un résultat similaire. Si on laisse tomber* en n'importe quel endroit sur terre une pièce de monnaie on ne sait pas précisément où celle-ci va tomber mais ce qui est sûr est qu'elle va se diriger vers le centre de la terre avant d'être arrêtée par le sol.

*: il faudrait préciser davantage les conditions de l'expérience car on peut m'objecter que si on fait fonctionner au même moment une soufflerie assez puissante, la pièce ne va pas tomber par terre mais s'envoler et tourbillonner.

PS.
Un ordinateur est une machine qui exploite un empilement de phénomènes physiques dont on sait prévoir l'issue, du moins suffisamment pour en faire quelque chose.

raoul.S

L'article est intéressant. En tout cas le bout gratuit qu'on peut lire. Il y a la question : Quelle sera alors la place des mathématiciens dans cette nouvelle distribution des rôles ?

Je pense qu'il est raisonnable de penser que dans les années à venir les "machines" prendront une place de plus en plus importante en math avec la découverte de "théorèmes" ou la preuve formelle de conjectures que les humains n'arrivent pas à résoudre.

Une chose qui ne disparaîtra pas de sitôt à mon avis est la capacité de l'humain à construire de l'abstraction via l'introduction de notions qui rendent les preuves formelles digestes. Une preuve formelle produite par une machine est une succession ignoble de caractères équivalent au langage machine en informatique.

En informatique on utilise des langages de programmation pour introduire de l'abstraction (par exemple langage orienté objets), puis on introduit de l'abstraction supplémentaire via les frameworks. C'est un peu comme ça que fonctionnent les humains qui font des maths j'ai l'impression. Ils créent des notions, des théories, l'équivalent d'un framework en informatique. D'ailleurs ce sont ces notions qui nous permettent d'apprécier réellement un résultat, et pas l'énoncé formel du résultat.

[Utilisateur supprimé]

@raoul.S

Je crois que les possibilités de la machine sont déjà très étudiés par les logiciens spécialistes en calculabilité. J'ai des lointains souvenirs en calculabilité, mais il me semble que la fonction "valeur de vérité" n'est pas calculable, ceci est déjà une grande limite de la machine face aux mathématiques.
Je pense que le rôle de la machine dans les mathématiques est très limité, mais qu'on ne se sert pas des machines jusqu'au bout de leur potentiel. À l'avenir, les machines serviront les mathématiciens à éviter les tâches trop mécaniques et répétitives.
 Il faudrait faire intervenir les spécialistes en calculabilité sur cette discussion.

Math Coss

@Foys : C'est un point que l'article dit explicitement : « Ce n’est pas la première fois qu’un assistant de preuve est utilisé, mais c’est la première fois qu’une preuve mathématique (ou, tout au moins, une partie) n’a pas été vérifiée par des humains à l’exception de ses auteurs, mais uniquement par une machine. » (En fait, je ne crois pas que ce soit vrai, c'était probablement le cas pour la démonstration de la conjecture de Kepler sur les empilements de sphères par Thomas Hales.)

@Dom : La confiance dans l'assistant de preuve repose sur le fait que c'est un logiciel formé d'un noyau relativement petit (quelques centaines de lignes), qu'un humain peut vérifier, et qui est capable de certifier progressivement le reste des constructions. Bien sûr, il est écrit en langage de haut niveau et il faut une certaine confiance dans le compilateur ou l'interpréteur dudit langage, laquelle vient du nombre de programmes qui fonctionnent déjà.

Foys

Igbinoba a dit :

il me semble que la fonction "valeur de vérité" n'est pas calculable,

En fait cette fonction n'existe même pas, c'est le théorème de Tarski qui le dit.

Les maths sont une sorte de graphe géant (infini) et (s'il est non contradictoire) si les machines ne peuvent pas apporter de réponse définitive à certaines questions (genre décider s'il y a une branche --une preuve- qui part d'un nœud donné-une phrase- et qui montre que cette branche est une preuve du nœud en gros), rien n'empêche a priori que ces machines n'exploreront une partie beaucoup plus grande de l'arbre que ce que l'humain peut faire, et ce beaucoup plus vite.

[Utilisateur supprimé]

Foys a dit :

En fait cette fonction n'existe même pas, c'est le théorème de Tarski qui le dit.

Pour tout langage du premier ordre $L$ et toute $L$-structure $\mathcal M$  tu peux définir par récursion transfinie une fonction qui à chaque formule close de $L_M$  associe sa valeur de vérité par rapport à la structure  $\mathcal M$. Je le sais car j'ai eu le loisir de définir cette fonction et en ce moment je fais des démos sur une version de cette fonction pour les formules du second ordre.
Il s'avère que cette fonction valeur de vérité (au premier ordre) n'est pas calculable en général. Aussi tu peux trouver des traces de cette fonction sur le David-Nour.
Édit : page 69 du David-Nour.

Foys

Igbinoba a dit :

Pour tout langage du premier ordre $L$ et toute $L$-structure $\mathcal M$  tu peux définir par récursion transfinie une fonction qui à chaque formule close de $L_M$  associe sa valeur de vérité par rapport à la structure  $\mathcal M$.

C'est moi qui mets en italique.

On ne sait même pas si pour les maths (les théories classiques qui en parlent telles que ZF, Peano ...) il existe au moins une telle $L$-structure, et pire, si jamais cette question est réellement tranchée un jour (par réellement je veux dire pas à coup d'extension de théories de plus en plus spéculatives) ce sera par la négative.

Soit $T$ une théorie permettant d'héberger les maths (c'est-à-dire récursive et entraînant les axiomes de l'arithmétique). On va supposer qu'on est en logique du premier ordre.

Alors il existe (constructivement) un énoncé $P$ tel que :

$T$ est contradictoire et n'est satisfaite par aucune $L$-structure, ou bien il existe deux $L$ structures satisfaisant $T$ (édité) telles que $P$ est vrai dans l'une et faux dans l'autre (vrai et faux s'entendent au sens de la fonction dont tu parles).

C'est le premier théorème de Gödel qui entraîne ça (plus le théorème de complétude pour prouver l'existence des $L$-structures en question; et pour l'impossibilité de trancher évoquée plus haut, le second).

Ce théorème n'est pas abordé mais seulement mentionné brièvement dans le livre de David,Nour et Raffali que tu cites.

Foys

Donc non, on ne peut pas parler de LA fonction de valeur de vérité (comme tu le fais en tout cas dans ton message).

Dom

Merci Math Coss pour cette réponse 👍

[Utilisateur supprimé]

Foys a dit : https://les-mathematiques.net/vanilla/index.php?p=/discussion/comment/2354442/#Comment_2354442

@Foys tu as mal interprété ce que j'ai dit, je ne parlais pas d'une fonction valeur de vérité générale, ma parole est toujours limitée et jamais généraliste.
Je parlais de la fonction valeur de vérité associée à une structure du premier ordre bien entendu, et je pensais que tout le monde aurait la même interprétation que moi, là j'ai eu tort.
Je connais les théorèmes d'incomplétude de Gödel, bien entendu, même si je ne les ai pas revu depuis longtemps. J'ai seulement cité le David-Nour car il était à côté de moi et que je savais qu'il parle de la fonction en question.

[Utilisateur supprimé]

Edit. Décidément, j'ai encore dit une bêtise concernant le théorème d'incomplétude que je n'ai pas revu depuis 10 ans au moins, je m'étais appuyé sur une version que j'avais trouvé sur wikipédia, et pourtant je sais qu'il faut se méfier de wikipédia.
Je suis allé voir le Cori-Lascar pour retrouver ce bon vieux théorème.
Et bien sûr ça change tout, on parle ici de théories récursives...
Ainsi, toute complétion de ZF ne serait pas récursive...la portée de ce théorème est bien moins grande que sa renommée.

raoul.S

Foys a dit :

rien n'empêche a priori que ces machines n'exploreront une partie beaucoup plus grande de l'arbre que ce que l'humain peut faire, et ce beaucoup plus vite.

Oui je pense que c'est ça qui va arriver. Et donc en gros cela signera la fin des matheux qui appartiennent à la catégorie des problem solver, et ce sera tout bénef pour les theory-builders auxquels appartenait un matheux très connu qui bénéficie d'un culte personnel par certains membres de ce forum...

PS. 

[Utilisateur supprimé]

@raoul.S tu parles de Christophe C ?

raoul.S

Oh non. CC est très bon mais il ne faut pas exagérer. D'ailleurs personne ne lui voue un culte que je sache (ou bien ? 🤔).

Non je parle de LUI.

PS. Une pensée pour toi CC...

[Utilisateur supprimé]

raoul.S 
Ah, ok, je croyais que tu parlais de quelqu'un du forum, et sachant que CC est un membre très respecté et qui a contribué beaucoup et que ses interventions manquent à beaucoup de membres du forum, j'ai tout de suite pensé que tu parlais de lui. Mais oui, en effet Alexandre Grothendieck est l'étoile filante des maths.

Et c'est presqu'un sacrilège de dire matheux en parlant de Grothendieck.

[Inutile de reproduire le message précédent. AD]

[Utilisateur supprimé]

Foys a dit : https://les-mathematiques.net/vanilla/index.php?p=/discussion/comment/2354441/#Comment_2354441

...$T$ est contradictoire et n'est satisfaite par aucune $L$-structure, ou bien il existe deux $L$ structures telles que $P$ est vrai dans l'une et faux dans l'autre...

Je viens de faire une relecture de cette phrase, et je pense que tu voulais dire ceci: "...$T$ est contradictoire et n'est satisfaite par aucune $L$-structure, ou bien il existe deux $T$-modèles tels que $P$ est vrai dans l'un et faux dans l'autre..."
Et comme j'ai dit précédemment, c'est une version erronée du théorème d'incomplétude.

Foys

Oui des $T$ modèles et si c'est juste (c'est entraîné par le théorème d'incomplétude mais n'est pas ledit théorème lui-même).

[Utilisateur supprimé]

@Foys
Je doute sérieusement que l'énoncé que tu as donné découle du théorème d'incomplétude de Gödel-Rosser.
En effet, ton énoncé aurait pour conséquence que si ZF est cohérent alors il ne peut être complété. Or, le langage de la théorie des ensembles est dénombrable donc si ZF est cohérent alors ZF peut être complété.

Je pense que les philosophes sont à l'origine de cette mauvaise interprétation du théorème d'incomplétude. Cette mauvaise interprétation est encore plus connue que le théorème lui même, et souvent les gens le confondent avec le théorème.

Foys

Igbinoba a dit :
En effet, ton énoncé aurait pour conséquence que si ZF est cohérent alors il ne peut être complété.

Ah bon, pourquoi?

[Utilisateur supprimé]

Sinon, pour réitérer ce que j'ai dit plus haut. Ce qu'on traite ici, c'est de la calculabilité.

[Utilisateur supprimé]

Foys a dit : https://les-mathematiques.net/vanilla/index.php?p=/discussion/comment/2354568/#Comment_2354568

[Inutile de recopier l'avant-dernier message. Un lien suffit. AD]

Édit : toute complétion de ZF permettra aussi d'héberger les maths.

Foys

@Igbinoba le problème est que cette complétion ne sera pas récursive.

[Utilisateur supprimé]

@Foys
T'avais mis "récursive" dans ton message de départ ? Si oui alors je ne l'avais pas vu.
Enfin bref, le théorème d'incomplétude montre plus une limitation de la machine qu'une limitation de ZF.

Foys

Igbinoba

S'engager dans des procès sans lire les petits caractères avant est généralement une mauvaise idée.

[Utilisateur supprimé]

@Foys en effet, j'aurais du faire plus attention. 
Cependant, ce qu'on peut retenir c'est que si ZF est cohérent alors aucune de ses complétions ne pourra être capturée par une machine. Voilà, ça fait 1 pour le mathématicien et zéro pour la machine.

raoul.S

ICI un article sur arXiv qui dit comment un réseau de neurones a pu trouver des contre-exemples à des conjectures ouvertes en théorie des graphes (je n'ai pas lu l'article juste l'introduction).

1 à 1 ?

pldx1

Il y a une forte nuance entre trouver un contre-exemple et prouver que personne ne trouvera de contre-exemples... parce qu'il n'en existe pas.
Trouver un contre-exemple consiste à trouver un sous ensemble-pertinent puis à mettre en oeuvre une méthode pertinente d'exploration. Il n'y a pas de nécessité d'établir cette double pertinence. Cela marche ou non... et on continue jusqu'au succès... qui ne viendra jamais s'il n'y a pas de contre-exemples: problème semi-décidable typique.
Quant aux mathématiciens qui n'aiment pas les ordinateurs face au défi des mathématiciens armés d'ordinateurs, on peut toujours faire comme si la réponse n'était pas évidente. Au passage: il y a plusieurs papiers de Michael Harris qui sont accessibles sur le net. Ils sont intéressants.

jean lismonde

Bonjour,
j'ai évoqué il y a peu, l'incertitude dans le calcul d'intégrales définies ou même de limites qui subsiste avec les calculatrices Premium qui sont pourtant recommandées aux élèves et étudiants.
Elles travaillent avec 11 chiffres significatifs (en fait 13) mais seuls les 6 premiers sont fiables.
C'est tout de même décevant.
Cordialement.

pldx1

Lorsque l'on utilise la formule de l'octroi pour un intégrande qui est infini aux bornes il faut s'attendre à une certaine déception. 
Evidemment, une véritable intelligence artificielle aurait répondu "tagouré-tagouré" plutôt que de se lancer dans les calculs.

raoul.S

pldx1 a dit :

Il y a une forte nuance entre trouver un contre-exemple et prouver que personne ne trouvera de contre-exemples... parce qu'il n'en existe pas.

Certes mais c'est un début. Voici une continuation. Un extrait (il s'agit d'une collaboration entre DeepMind et certains mathématiciens) :  

With Professor Lackenby and Professor Juhász, we explored knots - one of the fundamental objects of study in topology. Knots not only tell us about the many ways a rope can be tangled but also have surprising connections with quantum field theory and non-Euclidean geometry.  Algebra, geometry, and quantum theory all share unique perspectives on these objects and a long standing mystery is how these different branches relate: for example, what does the geometry of the knot tell us about the algebra? We trained an ML model to discover such a pattern and surprisingly, this revealed that a particular algebraic quantity — the signature — was directly related to the geometry of the knot, which was not previously known or suggested by existing theory. By using attribution techniques from machine learning, we guided Professor Lackenby to discover a new quantity, which we call the natural slope, that hints at an important aspect of structure overlooked until now. Together we were then able to prove the exact nature of the relationship, establishing some of the first connections between these different branches of mathematics.

[Et la traduction google. AD]

Avec le professeur Lackenby et le professeur Juhász, nous avons exploré les nœuds - l'un des objets d'étude fondamentaux en topologie. Les nœuds nous renseignent non seulement sur les nombreuses façons dont une corde peut être emmêlée, mais ont également des liens surprenants avec la théorie quantique des champs et la géométrie non euclidienne. L'algèbre, la géométrie et la théorie quantique partagent toutes des perspectives uniques sur ces objets et un mystère de longue date est la relation entre ces différentes branches : par exemple, que nous dit la géométrie du nœud sur l'algèbre ? Nous avons formé un modèle ML pour découvrir un tel modèle et, étonnamment, cela a révélé qu'une quantité algébrique particulière - la signature - était directement liée à la géométrie du nœud, qui n'était pas auparavant connue ou suggérée par la théorie existante. En utilisant des techniques d'attribution issues de l'apprentissage automatique, nous avons guidé le professeur Lackenby pour découvrir une nouvelle quantité, que nous appelons la pente naturelle, qui fait allusion à un aspect important de la structure négligé jusqu'à présent. Ensemble, nous avons alors pu prouver la nature exacte de la relation, établissant quelques-unes des premières connexions entre ces différentes branches des mathématiques.