Les algorithmes permettent-ils de fabriquer automatiquement des théorèmes ?

[andretou]

Bonjour à tous
Est-il vrai que l'on peut produire des théorèmes à la chaîne grâce aux algorithmes ?
Est-il correct que c'était l'ambition même du programme de Hilbert ?
Merci d'avance pour vos réponses
-----

[Deedee81]

Salut,

Est-il vrai que l'on peut produire des théorèmes à la chaîne grâce aux algorithmes ?

Oui et c'est même assez simple. A partir d'un jeu d'axiomes et en les combinants de toutes les manières possibles. Ou pour le dire autrement : c'est même très c.. à faire (désolé pour ce mot mais c'est vrai, c'est même plus facile que de programmer un jeu d'échec). Je le sais car j'ai fait les deux : algorithmes de génération automatique pour le jeu des chiffres et des lettres (et oui, on s'amuse comme on peu) et mon tout premier programme en basic était un programme d'échec (RD+R, sur TRS80, c'était déjà pas si mal).

Mais les théorèmes ainsi réalisés sont peu utiles car trop simples pour la plupart ou sans usage particulier. Et lorsqu'un intéressant se pointe il risque fort d'être noyés dans des milliards de théorèmes inutiles. Et il est évidemment par contre très difficile de savoir ce qu'est un bon théorème. Ce concept de bon résulte de considérations humaines difficiles à cerner et de l'usage possible, et difficile à voir à priori, de ce théorème dans des travaux dépassant le but initial de génération de théorèmes. On ne sait pas encore mettre le génie (mathématique ou autre) en bouteille.

C'est pourquoi les programmes de démonstration s'attaquent plutôt à une conjecture donnée et construisent le théorème par divers algorithmes pour accélérer la génération du théorème. Même comme cela ça reste très difficile et on combine généralement le travail humain et les programmes de démonstration : on découpe en sous-théorèmes, on cherche une ligne générale de démonstration en laissant les "petits" détails techniques à la machine ou on lui laisse le travail de "fourmi" (voir la démonstration de la conjecture de Kepler ou du théorème des 4 couleurs, la machine vérifiant juste des milliers de configurations de graphes qu'il serait extrêmement fastidieux de faire à la main). Ou alors on utilise des vérificateurs de preuves.

Est-il correct que c'était l'ambition même du programme de Hilbert ?

Non ce n'est pas correct.

Hilbert parlait bien de génération "automatique" ou plutôt d'algorithme comme une recette de cuisine (pas nécessairement exécutée par une machine, à part certaines machines de tri et les machines à tricoter, il n'y avait pas beaucoup d'ordinateur à l'époque). Mais pour toutes les propositions syntaxiquement correctes. C'est ça le but. Et Hilbert a montré que dès que la théorie est assez complexe (si elle inclut l'arithmétique par exemple) alors il y a des propositions qui ne peuvent être démontrées.

Ou pour le dire autrement : la machine va égrainer indéfiniment des théorèmes mais il en manquera toujours certains.

[Amanuensis]

Et Hilbert a montré que dès que la théorie est assez complexe (si elle inclut l'arithmétique par exemple) alors il y a des propositions qui ne peuvent être démontrées.

??? Erreur de frappe ? Pas plutôt "Gödel" que l'intention était de citer, et qu'un mécanisme indépendant de toute volonté a fait remplacer à la frappe par "Hilbert" ?

[Amanuensis]

Est-il vrai que l'on peut produire des théorèmes à la chaîne grâce aux algorithmes ?

Comme indiqué, c'est trivial, une fois posées un jeu d'axiomes et les règles de ré-écriture qu'on appelle "démontrer un théorème".

La difficulté est ailleurs : c'est par exemple le choix des axiomes !

[A voir en vidéo sur Futura]

[Deedee81]

??? Erreur de frappe ?

Lapsus plutôt Merci d'avoir rectifié.

La difficulté est ailleurs : c'est par exemple le choix des axiomes !

C'est juste.

Un jour j'avais vu un classement des activités mathématiques (il me semble que c'était dans un article de Delahaye) :
1. Il y a les calculateurs
2. Il y a les démonstrateurs
3. Il y a les créateurs de conjectures
4. Il y a les créateurs de théories (c'est-à-dire, des axiomes et des structures)

Ce classement est assez arbitraire car tout mathématicien touche peu ou prou aux différentes activités. Et chaque activité est indispensable à la discipline. Ce n'est pas un classement de valeur. Mais certains mathématiciens sont connus pour l'une ou l'autre de ces activités.

Les machines font très bien le 1, bien mieux que les humains même souvent dans le calcul formel pas que le numérique, on a fait de gros progrès dans le . mais les machines, sauf dans les démonstrations de type "fourmi" (au sens donné plus haut), ne valent toujours pas l'humain. Et en 3 et 4, les machines sont toujours médiocres. L'intuition, le savoir-faire, le "génie" peut-être, croit de 1 à 4. Les mathématiciens historiquement célèbre sont d'ailleurs ceux ayant obtenus de gros succès dans le 3 et le 4, parfois le 2. Mais la célébrité n'est jamais dans le 1 ce qui est dommage car sans calcul, pas de math et certains sont vraiment méritant (on leur rend parfois hommage, comme dans le film sur les "petites mains" du programme Appolo, ces femmes noires qui faisaient tous les calculs à la main et un peu oubliée à l'époque dans les honneurs des succès du programme : les raisons historiques ne sont bien sûr ici pas que liée au caractère "ingrat" et peu spectaculaire du calcul, inutile d'approfondir ce n'est pas le sujet).

Je ne doute pas que le 2 progressera encore (en IA). A quand un AlphaMath ? Mais pour le 3 et le 4, faudra probablement encore attendre un moment. Mais bon, on pourrait être surpris et j'ai cassé ma boule de crystal

[Médiat]

Bonjour,

Il y a un point non abordé et qui est pourtant le point fort des logiciels qui peuvent assister les mathématiciens, c'est la vérification de preuve (1.5 dans la liste ci-dessus).

Si les logiciels actuels pouvaient faire les démonstrations sans indication (en plus des axiomes), et en un temps acceptable, il y aurait une sacrée chouette lurette que les conjectures de Goldbach, des premiers jumeaux, de Syracuse, de Fermat en plus simple que Wiles etc. seraient résolues depuis longtemps

[Deedee81]

Il y a un point non abordé et qui est pourtant le point fort des logiciels qui peuvent assister les mathématiciens, c'est la vérification de preuve (1.5 dans la liste ci-dessus).

Je l'aurais plutôt mis dans le 1. Et c'est en effet une chose que font très bien les machines et c'est aussi une activité humaine (la vérification des démonstrations, c'est important, bien entendu).
(je l'avais cité dans le message 2 mais c'est vrai que je l'ai oublié dans la liste )

EDIT si je ne dis pas de bêtise on parle "d'assistant de preuve" (je fais référence à ton assister).
EDITbis, j'ai vérifié, c'est bien ça

Si les logiciels actuels pouvaient faire les démonstrations sans indication (en plus des axiomes), et en un temps acceptable, il y aurait une sacrée chouette lurette que les conjectures de Goldbach, des premiers jumeaux, de Syracuse, de Fermat en plus simple que Wiles etc. seraient résolues depuis longtemps

Je me demande si je verrai ça de mon vivant (pas seulement les démos mais une machine capable de le faire)

[andretou]

Merci beaucoup pour vos réponses !
Mais du coup je ne comprends pas l'intention de Hilbert avec son programme...
S'il ne cherchait pas à systématiser l'arithmétique, que cherchait-il donc à faire à travers son programme ?

[Deedee81]

Mais du coup je ne comprends pas l'intention de Hilbert avec son programme...
S'il ne cherchait pas à systématiser l'arithmétique, que cherchait-il donc à faire à travers son programme ?

Je l'ai dit plus haut : trouver un algorithme permettant de démontrer toute proposition (construite avec l'alphabet et les règles de syntaxe).
Toi ce que tu demandais est juste de lister un tas de démonstration.... ce qui n'est pas la même chose

[andretou]

Okay, j'ai compris !...
Merci Deedee !

[Amanuensis]

Mais du coup je ne comprends pas l'intention de Hilbert avec son programme...

Les intentions de Hilbert avaient une partie "métaphysique", sur la nature des maths. Le peu que j'ai lu des polémiques entre Poincaré et Hilbert sur le sujet montre une approche "philosophique" différentes des maths.

Autre manière de dire la même chose : on ne peut comprendre l'intention de Hilbert qu'en étudiant tout le contexte, pas en se focalisant sur ledit "programme".

Et la polémique a un rapport avec une autre toujours d'actualité sur la question si les maths sont "une construction humaine" ou "pré-existent et sont découvertes par les humains".

[Deedee81]

Utile à préciser :

https://fr.wikipedia.org/wiki/Probl%C3%A8mes_de_Hilbert

Peut-on prouver la cohérence de l'arithmétique ? En d'autres termes, peut-on démontrer que les axiomes de l'arithmétique ne sont pas contradictoires ?

La question ne se limite pas à l'énoncé de ces problèmes mais c'est vrai qu'initialement ce n'était pas juste "tout démontrer", j'avais été un peu vite, désolé.

[andretou]

Et la polémique a un rapport avec une autre toujours d'actualité sur la question si les maths sont "une construction humaine" ou "pré-existent et sont découvertes par les humains".

La question de savoir si les maths sont découvertes ou inventées par l'humanité était donc débattue par Hilbert et Poincarré ?
Sais-tu quels étaient leur avis respectifs sur la question ?

[Amanuensis]

La question de savoir si les maths sont découvertes ou inventées par l'humanité était donc débattue par Hilbert et Poincarré ?
Sais-tu quels étaient leur avis respectifs sur la question ?

Ce que j'en comprends est que Hilbert était côté "découverte" et Poincaré côté "invention". Pour Poincaré les maths sont d'abord un outil, construit pour l'usage des humains à des fins particulières. Pour Hilbert, la construction automatique est un mode d'exploration, de découverte.

La question en d'autres termes me semble être celle du choix des axiomes. Y a-t-il un jeu d'axiome "naturel", préexistant. Ou fabrique-t-on les jeux d'axiomes adaptés à des fins pratiques ? Je ne sais pas si P et H la voyait ainsi (l'idée d'axiomatique est très ancienne et sa formalisation, même si récente à leur époque, les précèdent).

[Médiat]

La question en d'autres termes me semble être celle du choix des axiomes. Y a-t-il un jeu d'axiome "naturel", préexistant. Ou fabrique-t-on les jeux d'axiomes adaptés à des fins pratiques ?

Il me semble qu'avant de ce poser la question d'un jeu d'axiome naturel (cf. les "errements" créatifs de Woodin, ou considérer le triplet ("Axiome du choix"(1) , "Théorème de Zermelo", "Lemme de Zorn") (dont chaque élément peut être pris comme axiome au "détriment" des autres), lequel serait plus naturel que les autres ?), il convient de se poser la question de la théorie (préexistante ou choisie adéquatement (3)), du langage (préexistant ou choisi adéquatement), et même peut-être du modèle (2) (préexistant ou choisi adéquatement)

(1) dans sa formulation usuelle
(2) formulation moderne, mais je suis sûr que cela reste clair
(3) j'ai repris l'idée de votre formulation, mais on pourrait aussi ajouter : contraint par la nature humaine

[andretou]

Mais au-delà des axiomes, des langages, des théories et des modèles (qui restent à choisir et/ou à déterminer), la base ultime de l'arithmétique n'est-elle pas le 0 et le 1 ?
En principe, ne suffit-il pas du 0 et du 1 pour reconstruire toute l'arithmétique et en connaître toutes les vérités ?
Autrement dit, le 0 et le 1 ne contiennent-ils pas à eux seuls toute l'arithmétique ?

[Médiat]

En principe, ne suffit-il pas du 0 et du 1 pour reconstruire toute l'arithmétique et en connaître toutes les vérités ?
Autrement dit, le 0 et le 1 ne contiennent-ils pas à eux seuls toute l'arithmétique ?

Non, et même un grand NON (les mathématiques avec mysticisme, c'est mal, très mal).

1) avec 0 et 1 sans axiome vous avez .... 0 et 1 (rien d'autres)
2) connaître toutes les vérités de l'arithmétiques, c'est Gödel lui-même qui vous dit non.

[andretou]

Mais avec seulement le 0 et le 1, on obtient pourtant la totalité des nombres, non ?...

[Amanuensis]

mais on pourrait aussi ajouter : contraint par la nature humaine

Oui, et c'est un point de vue assez fascinant.

Mon choix est surtout dû à ce que l'usage à des fins pratiques est difficilement opposable. Ce qu'est la nature humaine, et en discuter objectivement, est un sujet difficile.

[Médiat]

Mais avec seulement le 0 et le 1, on obtient pourtant la totalité des nombres, non ?...

ben non, avec 0, 1 seuls vous ne pouvez RIEN faire

[Amanuensis]

Supprimé .

[Médiat]

Oui, et c'est un point de vue assez fascinant.

Comme vous le savez, je partage pleinement cet avis

Ce qu'est la nature humaine, et en discuter objectivement, est un sujet difficile.

Là encore je suis bien d'accord, et c'est bien pourquoi j'ai choisi cette expression suffisamment vague

[andretou]

ben non, avec 0, 1 seuls vous ne pouvez RIEN faire

En définissant le nombre "deux" comme le 1 ajouté à lui-même, il me semble que je ne sollicite pas les axiomes de Peano puisqu'à ce stade la notion de successeur n'intervient pas... Est-ce que j'utiliserais alors d'autres axiomes sans m'en rendre compte ? Lesquels ?

[Médiat]

En définissant le nombre "deux" comme le 1 ajouté à lui-même, il me semble que je ne sollicite pas les axiomes de Peano puisqu'à ce stade la notion de successeur n'intervient pas... Est-ce que j'utiliserais alors d'autres axiomes sans m'en rendre compte ? Lesquels ?

Ceux de l'addition (donc un élément du langage et des axiomes)

[gg0]

Bonjour.

C'est quoi "ajouté"?
Bien évidement, on peut se contenter du "calcul" de l'école primaire, mais on ne fait pas de maths.

Cordialement

[Deedee81]

En définissant le nombre "deux" comme

Alors, contrairement à ce que tu disais, tu n'as pas que 0 et 1 puisque tu as déjà quelque chose en plus : la définition de deux (ou de l'addition comme le dit Médiat) (et si, c'est assez proche de ce qu'on a avec Peano, qu'on l'appelle "ajouté" comme toi ou successeur comme Peano. Pire encore : tu as besoin de 3, puis de 4... soit d'une infinité d'axiomes. C'est pas vraiment économe Et encore avec ça tu n'as que les nombres naturels et ce n'est une minuscule fraction de ce qui existe en mathématique). Et tu as pleins de choses en maths qui n'obéissent pas à ces axiomes d'addition ou de successeurs (c'est quoi le successeur d'une topologie ???).

Ah je m'autocorrige : tu ne parlais pas de toutes les maths mais seulement l'arithmétique, mais ça ne change rien : va voir la page wikipedia sur les axiomes de Peano, tu verras qu'il faut pas mal d'axiomes en plus pour avoir l'arithmétique, au-delà des simples nombres !!!

[Amanuensis]

En définissant le nombre "deux" comme le 1 ajouté à lui-même

On aurait alors même pas besoin du 1. Le zéro suffit ! Ce qui est encore plus drôle, le rien engendrant le non rien. (Bien sûr le principe créateur, c'est "ajouter 1", incrémenter !)

Mais cela c'est vision formelle, arithmétique. Les nombres ont d'abord un autre sens, celui du langage, ou de la "nature humaine" si on veut. Et à ce sens là ni 0 ni 1 ne sont des nombres, cela commence avec 2 (ce qui est à la fois pareil et différent). 2 et incrémenter, c'est la construction la plus élémentaire.

[Amanuensis]

Est-ce que j'utiliserais alors d'autres axiomes sans m'en rendre compte ? Lesquels ?

Déjà un à chaque fois qu'est introduite une nouvelle idée, un nouveau concept, un nouveau terme (mot) pertinent à l'arithmétique. Cela fait beaucoup.

[Médiat]

Les nombres ont d'abord un autre sens, celui du langage, ou de la "nature humaine" si on veut. Et à ce sens là ni 0 ni 1 ne sont des nombres, cela commence avec 2

Ce dernier point est totalement confirmé par l'histoire et bien éclairé par le premier point

[andretou]

Ok, admettons que pour définir "deux", j'ai besoin du 0 et du 1 (voire seulement du 0 selon Amanuensis, à débattre), et de quelque chose en plus que l'on nomme "addition".
Mais à ma connaissance l'addition n'est pas un concept axiomatique ; l'addition est décrite comme une "opération élémentaire", elle-même définie comme un "processus visant à obtenir un résultat à partir d'un ou plusieurs objets appelés opérandes"...
L'addition n'est donc pas un axiome (reste à définir son essence).
Autrement dit, avec le 0 et le 1, et avec l'addition, mais sans aucun axiome, on obtient bien la totalité des nombres, non ?...