Même s’il ne s’agit aucunement d’IA mais plutôt de semi-bruteforce, l’ordinateur a bien « produit » une connaissance nouvelle pour l’Homme.
Il doit être possible de faire de même pour de nombreux énoncés géométriques : Tarski a prouvé la complétude de la géométrie élémentaire et donc sa décidabilité : une théorie récursivement axiomatisable et complète est décidable (ce qui est globalement le cas d'une bonne partie des mathématiques que l'on apprend jusqu'au Bac).
En ce qui concerne l'ensemble de l'édifice mathématique, à la fin des années 50, les adeptes de l'IA prévoyaient le chômage pour les mathématiciens sous dix ans : force est de constater qu'ils ont échoué et qu'ils étaient fort présomptueux. On s'est alors plutôt orienté vers des assistants de preuves (les preuves sont semi-automatisées et guidées par le mathématicien) comme Coq, qui permettent également d'écrire des programmes « sans bugs » comme un compilateur, par exemple.
Pour ce qui est de la possibilité d'une intelligence artificielle, j'aurais tendance à rejoindre les vues de Jean-Yves Girard qu'il a exposées dans deux articles :
Il faut imaginer que l'on soit capable de créer un programme capable de résoudre un problème mathématique que l'on n'était nous même incapable de résoudre ?
Si l'humanité est capable de créer un tel programme, c'est qu'elle est capable de trouver un moyen pour résoudre le problème. Celui qui est intelligent, ce n'est ni le programme ni la machine qui le fait tourner, mais son auteur. ;-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: IA
Posté par kantien . En réponse au journal Un super ordinateur d'IA pour OpenAI. Évalué à 4.
Il doit être possible de faire de même pour de nombreux énoncés géométriques : Tarski a prouvé la complétude de la géométrie élémentaire et donc sa décidabilité : une théorie récursivement axiomatisable et complète est décidable (ce qui est globalement le cas d'une bonne partie des mathématiques que l'on apprend jusqu'au Bac).
En ce qui concerne l'ensemble de l'édifice mathématique, à la fin des années 50, les adeptes de l'IA prévoyaient le chômage pour les mathématiciens sous dix ans : force est de constater qu'ils ont échoué et qu'ils étaient fort présomptueux. On s'est alors plutôt orienté vers des assistants de preuves (les preuves sont semi-automatisées et guidées par le mathématicien) comme Coq, qui permettent également d'écrire des programmes « sans bugs » comme un compilateur, par exemple.
Pour ce qui est de la possibilité d'une intelligence artificielle, j'aurais tendance à rejoindre les vues de Jean-Yves Girard qu'il a exposées dans deux articles :
Et pour répondre à cette question :
Si l'humanité est capable de créer un tel programme, c'est qu'elle est capable de trouver un moyen pour résoudre le problème. Celui qui est intelligent, ce n'est ni le programme ni la machine qui le fait tourner, mais son auteur. ;-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.