Logique, explicabilité et compréhension future

Découverte liée à la logique

La logique est à la base de bien des choses. Mais quels sont les fondements de la logique elle-même?

Dans la logique symbolique, des symboles comme p et q sont introduits pour désigner des déclarations (ou «propositions») du type «ceci est un essai intéressant». Il existe encore certaines règles de logique, par exemple, pour tout p et tout q l'expression NOT (p AND q) est similaire à (NOT p) OR (NOT q).

Mais d'où viennent ces «règles de logique»? La logique est un système formel. Comme la géométrie euclidienne, elle peut être construite sur des axiomes. Mais que sont les axiomes? Vous pouvez commencer avec des instructions telles que p AND q = q AND p, ou NOT NOT p = p. Mais combien d'axiomes sont nécessaires? Comment peuvent-ils être simples?

Cette question est depuis longtemps douloureuse. Mais à 20h31 le dimanche 29 janvier 2000, le seul axiome est apparu sur l'écran de mon ordinateur. J'ai déjà montré que rien de plus simple, mais j'ai vite établi que ce seul petit axiome suffisait à créer toute la logique:


Comment savais-je qu'elle était vraie? Parce que je l'ai fait prouver à l'ordinateur. Et voici la preuve que j'ai imprimée dans le livre « A New Type of Science » (déjà disponible dans le référentiel Wolfram Data ):


En utilisant la dernière version de Wolfram Language, n'importe qui peut générer cette preuve en moins d'une minute. Et chacune de ses étapes est facile à vérifier . Mais pourquoi le résultat sera-t-il vrai? Comment l'expliquer?

Des questions similaires sont de plus en plus posées sur toutes sortes de systèmes informatiques et d'applications liés à l'apprentissage automatique et à l'IA. Oui, nous voyons ce qui se passe. Mais pouvons-nous comprendre cela?

Je pense que cette question est profondément inhérente - et d'une importance cruciale pour l'avenir de la science et de la technologie, et pour l'avenir de tout développement intellectuel.

Mais avant d'en parler, discutons de l'axiome que j'ai découvert.

L'histoire

La logique en tant que discipline formelle vient d'Aristote, qui a vécu au 4ème siècle avant JC. Dans le cadre de son travail de catalogage des choses (animaux, raisons, etc.), Aristote a compilé un catalogue de formes d'arguments autorisées et a créé des modèles symboliques pour eux, qui, en substance, ont fourni le contenu principal de la logique pour deux mille ans à venir.

Cependant, au 15ème siècle, l'algèbre a été inventée, et avec elle une image plus claire des choses est apparue. Mais ce n'est qu'en 1847 que George Bull a finalement formulé la logique de la même manière que l'algèbre, avec des opérations logiques telles que ET et OU fonctionnant selon des règles similaires aux règles de l'algèbre.

Après quelques années, les gens écrivaient déjà des systèmes axiomatiques pour la logique. Un exemple typique était:


Mais ET, OU et NON PAS vraiment nécessaires pour la logique? Après la première décennie du 20e siècle, plusieurs personnes ont découvert que la seule opération que nous appelons maintenant NAND suffira, et, par exemple, p OR q peut être calculé comme (p NAND p) NAND (q NAND q). La «complétude fonctionnelle» de la NAND pourrait toujours rester étrange sans le développement de la technologie des semi-conducteurs - elle implémente tous les milliards d'opérations logiques dans un microprocesseur moderne en utilisant une combinaison de transistors qui exécutent uniquement la fonction NAND ou le NOR associé.

Eh bien, à quoi ressemblent les axiomes de la logique en termes de NAND? En voici la première version connue, enregistrée par Henry Schaeffer en 1913 (ici le point désigne NAND):


En 1910, Principia Mathematica, un ouvrage en trois volumes sur la logique et la philosophie des mathématiques par Alfred North Whitehead et Bertrand Russell, a popularisé l'idée que peut-être toutes les mathématiques peuvent être déduites de la logique. Compte tenu de cela, il était assez intéressant d'étudier la question de la simplicité des axiomes de la logique. Le travail le plus important dans ce domaine a été effectué à Lviv et Varsovie (alors ces villes faisaient partie de la Pologne), en particulier, Jan Lukasevich (comme effet secondaire de son travail en 1920, il a inventé un record «polonais» qui ne nécessite pas de parenthèses). En 1944, à l'âge de 66 ans, Lukasevich a fui l'armée soviétique qui avançait et en 1947 a fini en Irlande.

Pendant ce temps, l'Irlandais Carew Meredith, qui a étudié à Winchester et à Cambridge et est devenu professeur de mathématiques à Cambridge, a été contraint de retourner en Irlande en 1939 en raison de son pacifisme. En 1947, Meredith a assisté à la conférence de Lukasevich à Dublin, qui l’a inspiré à rechercher des axiomes simples, ce qu’il a fait, pour la plupart, pour le reste de sa vie.

En 1949, Meredith a découvert un système à deux axiomes:


Près de 20 ans plus tard, en 1967, il a pu simplifier cela pour:


Est-il possible de simplifier davantage cela? Meredith a bricolé cela pendant des années, trouvant où vous pouvez supprimer la NAND supplémentaire. Mais après 1967, il n'a plus avancé (et est décédé en 1976), bien qu'en 1969 il ait trouvé un système à trois axiomes:


Quand j'ai commencé à étudier les systèmes axiomes de logique, je ne connaissais rien du travail de Meredith. Je me suis intéressé à ce sujet dans le cadre d'une tentative de comprendre quel comportement pourrait découler de règles simples. Dans les années 1980, j'ai découvert de façon inattendue que même les automates cellulaires avec les règles les plus simples possibles - comme ma règle préférée 30 - peuvent conduire à un comportement incroyablement complexe.

Ayant passé les années 1990 dans une tentative de comprendre la généralité de ce phénomène, j'ai finalement voulu voir comment il pouvait s'appliquer aux mathématiques. En mathématiques, nous commençons en fait à travailler avec des axiomes (par exemple, en arithmétique, en géométrie, en logique), puis sur leur base, nous essayons de prouver tout un ensemble de théorèmes complexes.

Cependant, à quel point les axiomes peuvent-ils être simples? C'est ce que je voulais établir en 1999. Comme premier exemple, j'ai décidé d'étudier la logique (ou, de manière équivalente, l'algèbre booléenne). Réfutant toutes mes attentes, mon expérience avec les automates cellulaires, les machines de Turing et d'autres systèmes - y compris les équations différentielles même partielles - suggère que vous pouvez simplement commencer à lister les cas les plus simples possibles et à un moment donné voir quelque chose intéressant.

Mais est-il possible «d'ouvrir la logique» de cette manière? Il n'y avait qu'une seule façon de le dire. Et fin 1999, j'ai tout arrangé pour commencer à explorer l'espace de tous les systèmes d'axiomes possibles, en commençant par le plus simple.

En un sens, tout système d'axiomes définit un ensemble de contraintes, disons, sur p · q. Elle ne dit pas ce qu'est p · q, elle ne donne que des propriétés que p · q doit satisfaire (par exemple, elle peut dire que q · p = p · q). La question est alors de savoir s'il est possible de déduire de ces propriétés tous les théorèmes de la logique qui tiennent lorsque p · q est Nand [p, q]: ni plus ni moins.

Quelque chose peut être vérifié directement. Nous pouvons prendre le système des axiomes et voir quelles formes p · q satisfont les axiomes, si p et q sont, disons, vrais et faux. Si le système des axiomes est que q · p = p · q, alors oui, p · q peut être Nand [p, q] - mais pas nécessairement. Il peut également s'agir de And [p, q] ou Equal [p, q], ou bien d'autres options qui ne satisfont pas aux mêmes niveaux que la fonction NAND en logique. Mais au moment où nous arrivons au système axiome {((p · p) · q) · (q · p) = q}, nous arrivons à l'état dans lequel Nand [p, q] (et l'équivalent de Nor [p , q]) restent les seuls modèles p · q qui fonctionnent - du moins si nous supposons que q et p n'ont que deux valeurs possibles.

S'agit-il alors d'un système d'axiomes pour la logique? Non. Parce que cela implique, par exemple, l'existence d'une variante où p et q ont trois valeurs, mais ce n'est pas dans la logique. Cependant, le fait que ce système d'axiomes d'un axiome soit proche de ce dont nous avons besoin indique qu'il vaut la peine de chercher un seul axiome à partir duquel la logique est reproduite. C'est exactement ce que j'ai fait en janvier 2000 (à notre époque, cette tâche a été facilitée grâce à la fonction assez nouvelle et très pratique de Wolfram Language, Groupements).

Il était assez facile de vérifier que les axiomes dans lesquels il y avait 3 NAND ou moins (ou «opérateurs de points») ne fonctionnaient pas. À 5 heures du matin le dimanche 29 janvier (oui, alors j'étais un hibou), j'ai découvert que les axiomes contenant 4 NAND ne fonctionneraient pas non plus. Lorsque j'ai arrêté de travailler vers 6 heures du matin, j'avais 14 candidats entre les mains de cinq NAND. Mais en continuant à travailler le dimanche soir et en effectuant des tests supplémentaires, j'ai dû tous les abandonner.

Inutile de dire que la prochaine étape consistait à vérifier les axiomes avec 6 NAND. Il y en avait 288 684. Mais mon code a fonctionné efficacement, et peu de temps s'est écoulé avant que les éléments suivants n'apparaissent à l'écran (oui, de Mathematica version 4):


Au début, je ne comprenais pas ce que je faisais. Je savais seulement que j'avais 25 axiomes non équivalents avec 6 NANDs qui ont pu avancer plus loin que les axiomes avec 5 NANDs. Mais y avait-il parmi eux des axiomes qui généraient de la logique? J'avais une méthode empirique capable d'éliminer les axiomes inutiles. Mais la seule façon de savoir avec certitude l'exactitude d'un axiome particulier était de prouver qu'il était capable de reproduire avec succès, par exemple, les axiomes de Schaeffer pour la logique.

Il a fallu un peu de jeu avec les programmes, mais après quelques jours, j'ai constaté que la plupart des 25 axiomes reçus ne fonctionnaient pas. En conséquence, deux ont survécu:



Et à ma grande joie, j'ai pu prouver à l'aide d'un ordinateur que les deux sont des axiomes de la logique. La technique utilisée garantit l'absence d'axiomes plus simples pour la logique. Par conséquent, je savais que j'avais atteint l'objectif: après un siècle (ou peut-être quelques millénaires) de recherches, nous pouvons enfin dire que nous avons trouvé l'axiome le plus simple de la logique.

Peu de temps après, j'ai découvert des systèmes de deux axiomes avec 6 NAND en général, qui, comme je l'ai prouvé, sont capables de reproduire la logique:



Et si nous prenons la commutativité p · q = q · p pour acquise, alors la logique peut être obtenue à partir de l'axiome contenant seulement 4 NAND.

Pourquoi est-ce important

Eh bien, disons que c'est très cool de pouvoir dire que quelqu'un "a terminé le travail commencé par Aristote" (ou du moins Boole) et a découvert le système d'axiomes le plus simple possible pour la logique. Est-ce juste un gadget, ou ce fait a-t-il des conséquences importantes?

Avant la plateforme que j'ai développée dans A New Kind of Science, je pense qu'il serait difficile de considérer ce fait comme quelque chose de plus qu'une simple curiosité. Mais maintenant, il devrait être clair qu'elle est liée à toutes sortes de questions fondamentales, telles que la question de savoir si les mathématiques doivent être considérées comme une découverte ou une invention.

Les mathématiques que les gens font sont basées sur une poignée de certains systèmes d'axiomes - chacun définissant un domaine spécifique des mathématiques (logique, théorie des groupes, géométrie, théorie des ensembles). Mais en parlant de façon abstraite, il existe un nombre infini de systèmes d'axiomes - chacun définissant un domaine des mathématiques qui peut être étudié, même si les gens ne l'ont pas encore fait.

Avant le livre A New Kind of Science, je voulais dire que tout ce qui existe «quelque part là-bas» dans l'univers informatique devrait être «moins intéressant» que ce que les gens ont créé et étudié. Mais mes découvertes concernant les programmes simples indiquent que les systèmes qui «simplement quelque part là-bas» n'ont pas des possibilités moins riches que ces systèmes soigneusement sélectionnés par les gens.

Alors qu'en est-il du système axiome pour les mathématiques? Pour comparer le «quelque part là-bas» existant avec ce que les gens ont étudié, vous devez savoir si les systèmes axiomatiques se situent dans les domaines mathématiques existants que nous avons étudiés. Et, sur la base des systèmes traditionnels créés par les gens, nous pouvons conclure qu'ils doivent être quelque part très, très loin - et en général, ils ne peuvent être trouvés que si vous savez déjà où vous êtes.

Mais ma découverte du système des axiomes a répondu à la question "Jusqu'où est la logique?" Pour des choses comme un automate cellulaire, il est assez facile de numéroter (comme je l'ai fait dans les années 1980) tous les automates cellulaires possibles. C'est un peu plus difficile à faire avec les systèmes axiomes - mais pas de beaucoup. Dans une approche, mon axiome peut être noté 411; 3; 7; 118 - ou, dans Wolfram Language:


Et, au moins dans l'espace des formes fonctionnelles possibles (sans tenir compte du balisage des variables), il y a une représentation visuelle de l'emplacement de cet axiome:


Étant donné l'importance fondamentale de la logique pour un si grand nombre de systèmes formels que les gens étudient, on pourrait penser que dans toute représentation raisonnable, la logique correspond à l'un des systèmes d'axiomes les plus simples possibles. Mais, au moins dans une présentation utilisant NAND, ce n'est pas le cas. Pour elle, il existe toujours un système d'axiomes très simple, mais il se révélera probablement être cent mille systèmes d'axiomes parmi tous ceux qui peuvent être trouvés si vous commencez simplement à numéroter le système d'axiomes, en commençant par le plus simple.

Compte tenu de cela, la prochaine question évidente sera: qu'en est-il de tous les autres systèmes d'axiomes? Comment se comportent-ils? C'est ce numéro que le livre A New Kind of Science explore. Et j'y affirme que les choses telles que les systèmes observés dans la nature sont le plus souvent décrites par ces «autres règles» que nous pouvons trouver en numérotant les possibilités.

Quant aux systèmes d'axiomes, j'ai fait un tableau représentant ce qui se passe dans les "domaines des mathématiques" correspondant aux différents systèmes d'axiomes. La série montre les conséquences d'un certain système d'axiomes, et les encadrés indiquent la vérité d'un certain théorème dans un système donné d'axiomes (oui, à un moment donné le théorème de Gödel entre en vigueur, après quoi il devient incroyablement difficile de prouver ou de réfuter un théorème donné dans un système donné d'axiomes; en pratique, avec par mes méthodes, cela se produit un peu à droite de ce qui est montré dans l'image).


Y a-t-il quelque chose de fondamentalement spécial dans les domaines des mathématiques qui sont «recherchés par les gens»? À en juger par cette photo et d'autres, rien d'évident ne vient à l'esprit. Je soupçonne qu'il n'y a qu'une seule caractéristique dans ces domaines - le fait historique qu'ils ont été étudiés. (Vous pouvez faire des déclarations comme «elles décrivent le monde réel» ou «liées au fonctionnement du cerveau», mais les résultats décrits dans le livre suggèrent le contraire).

Eh bien, quelle est la signification de mon système d'axiomes pour la logique? Sa taille vous fait sentir le contenu final de l'information de la logique en tant que système axiomatique. Et cela nous oblige à considérer - au moins pour l'instant - que nous devons considérer la logique plus comme une «construction inventée par l'homme» que comme une «découverte» qui s'est produite pour des «raisons naturelles».

Si l'histoire se déroulait différemment et que nous cherchions constamment (comme cela est fait dans le livre) de nombreux systèmes d'axiomes les plus simples possibles, alors nous ouvririons probablement le système des axiomes à la logique, comme le système dont nous trouvons les propriétés intéressantes. Mais puisque nous avons étudié un si petit nombre de tous les systèmes d'axiomes possibles, je pense qu'il serait raisonnable de considérer la logique comme une «invention» - une construction spécialement créée.

Dans un sens, au Moyen Âge, la logique ressemblait à ceci - lorsque les syllogismes possibles (types d'arguments acceptables) étaient représentés sous la forme de mnémoniques latins comme bArbArA et cElErAnt. Par conséquent, il est maintenant intéressant de trouver une représentation mnémonique de ce que nous connaissons maintenant comme le système d'axiomes le plus simple pour la logique.

À partir de ((p · q) · r) · (p · ((p · r) · p)) = r, chaque p · q peut être représenté comme un préfixe ou une entrée polonaise (inverse à "l'entrée polonaise inversée" de la calculatrice HP ) sous la forme de Dpq - par conséquent, l'axiome entier peut être écrit comme = DDDpqrDpDDprpr. Il existe également un mnémonique anglais sur ce sujet - FIGURE OuT Queue, où les rôles p, q, r sont joués par u, r, e. Ou vous pouvez regarder les premières lettres des mots dans la phrase suivante (où B est l'opérateur, et p, q, r sont a, p, c): «Petit à petit, un programme a calculé le meilleur axiome binaire de l'algèbre booléenne couvrant tous les cas» [ le meilleur axiome binaire de l'algèbre de Boole calculé au moyen d'un programme décrit progressivement tous les cas].

Mécanique de la preuve

D'accord, alors comment prouvez-vous l'exactitude de mon système d'axiomes? La première chose qui vient à l'esprit est de montrer qu'il est possible d'en déduire un système bien connu d'axiomes pour la logique - par exemple, le système d'axiomes de Schaeffer:


Il y a trois axiomes ici, et nous devons en dériver chacun. Voici ce que vous pouvez faire pour générer le premier, en utilisant la dernière version de Wolfram Language:


Il convient de noter qu'il est désormais possible de le faire. Dans «l'objet de la preuve», il est écrit que 54 étapes ont été utilisées pour la preuve. Sur la base de cet objet, nous pouvons générer un «cahier» qui décrit chacune des étapes:


En général, toute la séquence des lemmes intermédiaires est prouvée ici, ce qui nous permet de déduire le résultat final. Entre les lemmes, il y a tout un réseau de dépendances mutuelles:


Mais les réseaux impliqués dans la dérivation des trois axiomes dans le système d'axiomes de Scheffer - pour ce dernier, 504 étapes incroyables sont utilisées:


Oui, il est évident que ces réseaux sont assez déroutants. Mais avant de discuter de ce que signifie cette complexité, parlons de ce qui se passe à chaque étape de cette preuve.

L'idée principale est simple. Imaginez que nous ayons un axiome qui est simplement écrit comme p · q = q · p (mathématiquement, cela signifie que l'opérateur est commutatif). Plus précisément, l'axiome dit que pour toute expression p et q, p · q est équivalent à q · p.

Eh bien, disons que nous voulons déduire de cet axiome que (a · b) · (c · d) = (d · c) · (b · a). Cela peut être fait en utilisant l'axiome pour convertir d · c en c · d, b · a en a · b, et enfin (c · d) · (a · b) en (a · b) · (c · d )

FindEquationalProof fait essentiellement la même chose, bien qu'il ne suive pas ces étapes exactement dans le même ordre et change à la fois le côté gauche de l'équation et le droit.


Après avoir reçu une telle preuve, vous pouvez simplement suivre chaque étape et vérifier qu'elles donnent le résultat indiqué. Mais comment trouver des preuves? Il existe de nombreuses séquences possibles de permutations et de transformations. Comment trouver une séquence qui amène avec succès au résultat final?

On pourrait décider: pourquoi ne pas essayer toutes les séquences possibles, et s'il y a une séquence de travail parmi elles, elle devrait finalement être trouvée?Le problème est que vous pouvez arriver rapidement à un nombre astronomique de séquences. L'essentiel de l'art de prouver automatiquement les théorèmes consiste à trouver des moyens de réduire le nombre de séquences à vérifier.

Cela se glisse rapidement dans les détails techniques, mais l'idée de base est facile à discuter si vous connaissez les bases de l'algèbre. Supposons que nous essayons de prouver un résultat algébrique comme


Il existe un moyen garanti de le faire: en appliquant simplement les règles de l'algèbre pour révéler chaque côté, vous pouvez immédiatement voir leur similitude:


Pourquoi ça marche?Parce qu'il existe un moyen de travailler avec de telles expressions, en les réduisant systématiquement jusqu'à ce qu'elles prennent une forme standard. Est-il possible de faire la même opération dans des systèmes arbitraires d'axiomes?

Pas tout de suite. En algèbre, cela fonctionne car il possède une propriété spéciale qui garantit que vous pouvez toujours «vous déplacer» le long du chemin de la simplification des expressions. Mais dans les années 1970, différents scientifiques ont découvert à plusieurs reprises de manière indépendante (sous des noms comme l'algorithme de Knuth-Bendix ou la base de Gröbner ) que même si le système axiomatique n'a pas la propriété interne nécessaire, il est possible de découvrir des «ajouts» à ce système dans lequel il il y en a.

C’est ce qui se produit dans les preuves typiques fournies par FindEquationalProof (basé sur le système de Valdmeister, «maître des arbres»). Il y a ce qu'on appelle Les «lemmes à couple critique», qui ne font pas directement avancer la preuve, mais permettent l'émergence de chemins capables de cela. Tout est compliqué du fait que, bien que l'expression finale que nous voulons obtenir soit assez courte, sur le chemin, vous devrez peut-être passer par des expressions intermédiaires beaucoup plus longues. Par conséquent, par exemple, la preuve du premier axiome de Schaeffer comporte de telles étapes intermédiaires:


Dans ce cas, la plus grande des étapes est 4 fois plus grande que l'axiome d'origine:


Ces expressions peuvent être représentées comme un arbre. Voici son arbre, comparé à l'arbre de l'axiome original:


Et c'est ainsi que se développent les tailles des étapes intermédiaires au cours des preuves de chacun des axiomes de Schaeffer:

Pourquoi est-ce si difficile?

Faut-il s'étonner que ces preuves soient si complexes? Pas vraiment, vraiment. Après tout, nous savons bien que les mathématiques peuvent être complexes. En principe, il se pourrait que toutes les vérités mathématiques soient faciles à prouver. Mais l'un des effets secondaires du théorème de Gödel de 1931 est que même les choses qui ont des preuves, leur chemin peut être arbitrairement long.

C'est le symptôme d'un phénomène beaucoup plus général, que j'appelle irréductibilité informatique . Considérons un système contrôlé par une simple règle d'un automate cellulaire (bien sûr, dans tous mes essais, il y aura toujours des automates cellulaires). Exécutez ce système.


Il pourrait être décidé que si le système est basé sur une règle simple, il devrait y avoir un moyen rapide de comprendre ce que fait le système. Mais ce n'est pas le cas.Selon mon principe d'équivalence de calcul , le fonctionnement d'un système correspond souvent à des calculs dont la complexité coïncide avec tous les calculs que nous pourrions faire pour comprendre le comportement du système. Cela signifie que le comportement réel du système correspond en fait à une telle quantité de travail de calcul, qui ne peut en principe pas être réduit.

En ce qui concerne l'image ci-dessus: disons que nous voulons savoir si le motif meurt à la fin. Nous pourrions continuer à le remplir, et si nous avons de la chance, il finira par dégénérer en quelque chose, dont le sort sera évident. Cependant, en général, il n'y a pas de limite supérieure sur le temps que nous devons consacrer, en fait, à la preuve.

Lorsque quelque chose comme cela se produit avec des preuves logiques, cela se produit un peu différemment. Au lieu de commencer quelque chose qui fonctionne selon certaines règles, nous demandons s'il existe un moyen d'atteindre un certain résultat en passant par plusieurs étapes, chacune obéissant à une certaine règle. Et cette tâche, en tant que tâche de calcul pratique, est beaucoup plus compliquée. Mais l'essence de la complexité est le même phénomène d'irréductibilité informatique, et ce phénomène suggère qu'il n'y a pas de moyen général de contourner brièvement le processus d'étude de ce que le système fera.

Inutile de dire qu'il y a beaucoup de choses dans le monde - en particulier dans la technologie et la modélisation scientifique, ainsi que dans les domaines où il existe différentes formes de règles - traditionnellement conçues pour éviter l'irréductibilité informatique et pour travailler de sorte que le résultat de leur travail soit immédiatement visible, sans avoir à effectuer une quantité irréductible de calculs.

Mais l'une des conséquences de mon principe d'équivalence informatique est que ces cas sont singuliers et non naturels - il soutient que l'irréductibilité informatique existe dans tous les systèmes de l'univers informatique.

Et les mathématiques? Peut-être que les règles des mathématiques sont spécifiquement choisies pour démontrer la réductibilité du calcul. Et dans certains cas, c'est le cas (et dans un sens, cela se produit également en logique). Mais pour la plupart, il semble que les systèmes d'axiomes des mathématiques ne soient pas atypiques pour l'espace de tous les systèmes possibles d'axiomes - où l'irréductibilité informatique est endémique.

Pourquoi avons-nous besoin de preuves?

Dans un sens, une preuve est nécessaire pour connaître la vérité de quelque chose. Bien sûr, surtout à notre époque, les preuves ont disparu dans le fond, laissant la place au calcul pur. En pratique, le désir de générer quelque chose par des calculs est beaucoup plus courant que le désir de «prendre du recul» et de construire une preuve de la vérité de quelque chose.

En mathématiques pures, cependant, il faut souvent faire face à des concepts qui incluent, au moins nominalement, un nombre infini de cas («vrai pour tous les nombres premiers», etc.) pour lesquels les calculs du front ne fonctionneront pas. . Et lorsque la question se pose de confirmer ("ce programme peut-il se terminer avec une erreur?" Ou "puis-je dépenser cette crypto-monnaie deux fois?") Il est plus raisonnable d'essayer de le prouver que de calculer tous les cas possibles.

Mais dans la pratique mathématique réelle, la preuve est plus que l'établissement de la vérité. Quand Euclide a écrit ses « débuts », il a simplement indiqué les résultats et «les a laissés au lecteur». Mais, d'une manière ou d'une autre, en particulier au cours du siècle dernier, les preuves se sont transformées en quelque chose qui ne se produit pas seulement dans les coulisses, mais est le principal moyen par lequel il est nécessaire de diffuser des concepts.

Il me semble qu'en raison de quelque bizarrerie de l'histoire, les preuves sont offertes aujourd'hui comme un objet que les gens devraient comprendre, et les programmes sont considérés comme quelque chose qu'un ordinateur devrait exécuter. Pourquoi est-ce arrivé? Eh bien, au moins dans le passé, les preuves pouvaient être présentées sous forme de texte - donc, si quelqu'un l'utilisait, alors seulement les gens. Et les programmes étaient presque toujours enregistrés sous la forme d'un langage informatique. Et pendant très longtemps, ces langages ont été créés afin de pouvoir se traduire plus ou moins directement en opérations informatiques de bas niveau - c'est-à-dire que l'ordinateur les a compris immédiatement, mais les gens n'ont pas à le faire.

Mais l'un des principaux objectifs de mon travail au cours des dernières décennies a été de changer cet état de fait et de développer dans Wolfram Language un véritable "langage de communication informatique" dans lequel les idées informatiques peuvent être transmises afin qu'elles puissent être comprises par les ordinateurs et les personnes.

Une telle langue a de nombreuses conséquences. L'un d'eux change le rôle des preuves. Supposons que nous regardions un résultat mathématique. Dans le passé, le seul moyen plausible de le faire comprendre était de donner la preuve que les gens lisaient. Mais maintenant, une autre chose est possible: vous pouvez distribuer un programme pour Wolfram Language qui calcule le résultat. Et c'est à bien des égards un moyen beaucoup plus riche de transmettre la vérité du résultat. Chaque partie du programme est quelque chose de précis et sans ambiguïté - tout le monde peut commencer. Il n'y a pas de problème tel que les tentatives de comprendre une partie du texte, nécessitant de combler certaines lacunes. Tout est clairement indiqué dans le texte.

Et les preuves? Existe-t-il des moyens clairs et précis de rédiger des preuves? Potentiellement oui, bien que ce ne soit pas particulièrement facile. Et bien que la fondation Wolfram Language existe depuis 30 ans, ce n'est qu'aujourd'hui qu'un moyen raisonnable a semblé présenter des preuves structurelles simples, comme l'un de mes axiomes ci-dessus.

Vous pouvez imaginer créer des preuves dans Wolfram Language de la même manière que les gens créent des programmes - et nous travaillons pour fournir des versions de haut niveau de cette fonctionnalité qui «aident à la preuve». Cependant, personne n'a créé la preuve de mon système d'axiomes - un ordinateur l'a trouvée. Et cela ressemble plus à la sortie du programme qu'au programme lui-même. Cependant, comme un programme, dans un sens, la preuve peut également être «exécutée» pour vérifier le résultat.

Créer de la clarté

La plupart du temps, les personnes utilisant le Wolfram Language, ou Wolfram | Alpha, veulent compter quelque chose. Ils doivent obtenir le résultat, ne pas comprendre pourquoi ils ont obtenu de tels résultats. Mais dans Wolfram | Alpha, en particulier dans des domaines tels que les mathématiques et la chimie, une caractéristique populaire parmi les étudiants est la construction de solutions "étape par étape".


Lorsque le système Wolfram | Alpha calcule, par exemple, une intégrale, il utilise toutes sortes de techniques algorithmiques puissantes qui sont optimisées pour recevoir des réponses. Mais quand on lui demande de montrer les étapes des calculs, elle fait autre chose: elle doit expliquer par étapes pourquoi c'est le résultat obtenu.

Il n'y aurait aucun avantage à expliquer comment le résultat a été obtenu; Il s'agit d'un processus très inapproprié pour les humains. Elle doit comprendre quelles opérations apprises par les gens peuvent être utilisées pour obtenir un résultat. Souvent, elle trouve une astuce utile. Oui, elle a un moyen systématique de le faire, qui fonctionne toujours. Mais il y a trop d'étapes "mécaniques". Une «astuce» (substitution, intégration partielle, etc.) ne fonctionnera pas dans le cas général, mais dans ce cas particulier, elle donnera un moyen plus rapide à la réponse.

Qu'en est-il d'obtenir des versions claires d'autres choses? Par exemple, le travail des programmes dans le cas général. Ou des preuves de mon système axiome.

Commençons par les programmes. Supposons que nous ayons écrit un programme et que nous voulions expliquer comment il fonctionne. L'une des approches traditionnelles consiste à inclure des commentaires dans le code. Si nous écrivons dans une langue traditionnelle de bas niveau, c'est peut-être la meilleure solution. Mais l'essence même de Wolfram Language en tant que langage de communication informatique est que le langage lui-même devrait permettre la transmission d'idées, sans avoir besoin d'inclure des morceaux de texte supplémentaires.

Des efforts doivent être faits pour faire du programme Wolfram Language une bonne description du processus, ainsi que pour faire du texte anglais clair une bonne description du processus. Cependant, vous pouvez obtenir un morceau de code Wolfram Language qui explique très clairement comment tout fonctionne de manière autonome.

Bien sûr, il arrive souvent que l'exécution réelle du code mène à des choses qui ne découlent évidemment pas du programme. Je mentionnerai bientôt les cas extrêmes comme les automates cellulaires. Mais pour l'instant, imaginons que nous avons créé un programme par lequel nous pouvons imaginer ce qu'il fait généralement.

Dans ce cas, j'ai trouvé que les essais informatiques présentés sous forme de cahiers Wolfram sont un excellent outil pour expliquer ce qui se passe. Il est important que Wolfram Language, cela vous permet d'exécuter même les plus petites parties de programmes séparément (avec les expressions symboliques correspondantes en tant que données d'entrée et de sortie). Après cela, vous pouvez imaginer la séquence des étapes du programme comme une séquence d'éléments du dialogue qui constitue la base du bloc-notes informatique.

En pratique, il est souvent nécessaire de créer des visualisations des données d'entrée et de sortie. Oui, tout peut être exprimé comme une représentation symbolique sans ambiguïté. Mais il est beaucoup plus facile pour les gens de comprendre la représentation visuelle des choses que toute ligne unidimensionnelle semblable à un langage.

Bien sûr, créer de bonnes visualisations s'apparente à de l'art. Mais chez Wolfram Language, nous avons fait beaucoup de travail pour automatiser cet art - souvent à l'aide d'un apprentissage automatique assez sophistiqué et d'autres algorithmes qui effectuent des choses comme la disposition des réseaux ou des éléments graphiques.

Et si on commençait par un simple suivi de programme? C'est difficile à faire. J'expérimente cela depuis des décennies et je n'ai jamais été complètement satisfait des résultats. Oui, vous pouvez zoomer et voir de nombreux détails de ce qui se passe. Mais je n'ai pas trouvé suffisamment de bonnes techniques pour comprendre l'ensemble de l'image et donner automatiquement des choses particulièrement utiles.

À un certain niveau, cette tâche est similaire à la rétro-ingénierie. On vous montre un code machine, un circuit à puce, peu importe. Et vous devez prendre du recul et recréer la description de haut niveau à partir de laquelle la personne repoussée, qui en quelque sorte «compilé» dans ce que vous voyez.

Dans l'approche traditionnelle de l'ingénierie, lorsque les gens créent un produit par étapes, ayant toujours la capacité d'anticiper les conséquences de ce qu'ils créent, cette approche peut fonctionner en principe. Mais si au lieu de cela vous vous promenez dans l'univers informatique à la recherche d'un programme optimal (comme je cherchais des systèmes d'axiomes possibles pour trouver un système de logique), il n'y a aucune garantie qu'il y aura une "histoire humaine" ou une explication derrière ce programme.

Un problème similaire se rencontre dans les sciences naturelles. Vous voyez comment un ensemble complexe de toutes sortes de processus se développe dans un système biologique. Est-il possible de les soumettre à une «rétro-ingénierie» afin de trouver une «explication»? On peut parfois dire que l'évolution avec la sélection naturelle y conduira. Ou qu'il se trouve souvent dans l'univers informatique, de sorte que la probabilité de son occurrence est élevée. Mais rien ne garantit que le monde naturel est nécessairement conçu pour que les gens puissent l'expliquer.

Naturellement, lors de la modélisation des choses, nous ne considérons inévitablement que les aspects qui nous intéressent et idéalisons tout le reste. Et surtout dans des domaines comme la médecine, vous devez souvent travailler avec un modèle approximatif avec un arbre de décision peu profond, ce qui est facile à expliquer.

La nature de l'explicabilité

Que signifie l'expression «quelque chose peut être expliqué»? Essentiellement, cela signifie que les gens peuvent le comprendre.

Que faut-il aux gens pour comprendre quelque chose? Nous devons en quelque sorte réaliser cela. Prenez un automate cellulaire typique avec un comportement complexe. L'ordinateur n'a pas de problèmes pour passer par toutes les étapes de son évolution. Avec des efforts et un travail énormes, une personne pourrait reproduire le travail d'un ordinateur.

Mais on ne peut pas dire que dans ce cas, une personne "comprendrait" ce que fait un automate cellulaire. Pour cela, une personne devrait facilement parler du comportement d'un automate cellulaire à un niveau élevé. Ou, en d'autres termes, une personne devrait être capable de «raconter une histoire» sur le comportement d'un automate que d'autres personnes pourraient comprendre.

Existe-t-il un moyen universel de procéder? Non, en raison de l'irréductibilité informatique. Cependant, il peut arriver que certaines fonctionnalités importantes pour les utilisateurs puissent être expliquées à un niveau élevé avec certaines limitations.

Comment ça marche? Pour ce faire, vous devez créer un certain langage de haut niveau qui peut décrire les fonctionnalités qui nous intéressent. En étudiant un dessin typique de l'automate cellulaire, on peut essayer de parler non pas en termes de couleurs d'un grand nombre de cellules individuelles, mais en termes de structures d'un niveau supérieur qui peuvent être détectées. L'essentiel est que vous puissiez compiler au moins un catalogue partiel de telles structures: bien qu'il y ait beaucoup de détails qui ne rentrent pas dans la classification, certaines structures sont courantes.

Et si nous voulons commencer à «expliquer» le comportement d'un automate cellulaire, nous commencerons par nommer les structures, puis nous parlerons de ce qui se passe du point de vue de ces structures.


Le cas de l'automate cellulaire a une caractéristique simplificatrice: puisqu'il fonctionne sur la base de règles déterministes simples, il a des structures également répétitives. Dans la nature, par exemple, nous ne rencontrons généralement pas une répétition aussi identique. Il n'y a qu'un seul, par exemple, un tigre, très similaire à l'autre, c'est pourquoi nous les appelons tous les deux «tigres», bien que la disposition de leurs atomes ne soit pas identique.

Quelle est la signification générale de tout cela? Elle consiste à utiliser l'idée de représentation symbolique. Nous disons que nous pouvons attribuer un certain symbole - souvent ce mot - qui peut être utilisé pour décrire symboliquement toute une classe de choses, sans avoir à énumérer en détail chaque détail de tous les composants de ces choses.

Ceci est similaire à la compression d'informations: nous utilisons des constructions symboliques pour trouver une manière plus courte de décrire les choses qui nous intéressent.

Supposons que nous ayons généré une structure gigantesque, par exemple mathématique:


La première étape consiste à créer une sorte de représentation interne de haut niveau. Par exemple, nous pouvons détecter des structures réutilisables. Et nous pouvons leur donner des noms. Et puis montrez le "squelette" de la structure entière avec leur aide:


Oui, ce schéma, similaire à la «compression de dictionnaire», est utile pour atteindre le premier niveau d'explicabilité.

Mais revenons à la preuve de mon système d'axiomes. Les lemmes créés dans cette épreuve sont spécialement sélectionnés comme éléments réutilisables. Cependant, en les excluant, il nous reste des preuves que les gens ne peuvent pas comprendre immédiatement.

Que pouvez-vous faire d'autre? Nous devons trouver une sorte de description d'un niveau encore plus élevé. Qu'est-ce que ça pourrait être?

Concept de concepts

Si vous essayez d'expliquer quelque chose à quelqu'un, il sera beaucoup plus facile de le faire si vous trouvez autre chose, mais similaire qu'une personne pourrait déjà comprendre. Imaginez comment vous expliquerez le concept d'un drone moderne à une personne de l'âge de pierre. Ce sera difficile à faire. Mais il sera beaucoup plus facile d'expliquer cela à une personne qui vivait il y a 50 ans et qui a déjà vu des hélicoptères et des modèles réduits d'avions.

Et à la fin, l'essentiel est que lorsque nous expliquons quelque chose, nous le faisons dans une langue connue de nous et de celle à qui nous l'expliquons. Et plus la langue est riche, moins nous devons introduire de nouveaux éléments pour transmettre ce que nous essayons d'expliquer.

Il y a un modèle qui se répète tout au long de l'histoire de l'esprit. Un certain ensemble de choses sont remarquées plusieurs fois. Peu à peu, ils commencent à comprendre que ces choses sont en quelque sorte abstraitement similaires, et toutes peuvent être décrites en termes d'un nouveau concept, qui est décrit dans un nouveau mot ou une phrase.

Supposons que nous remarquions des choses comme l'eau, le sang et l'huile. À un certain moment, nous comprenons qu'il existe un concept généralisé de «liquide», et tous peuvent être décrits comme liquides. Et quand nous avons un tel concept, nous pouvons commencer à raisonner en ses termes, en trouvant plus de concepts - disons la viscosité, basés sur lui.

Quand est-il judicieux de combiner les choses en un concept? Une question difficile à laquelle on ne peut répondre sans prévoir tout ce qui peut être fait avec ce concept. En pratique, dans le processus d'évolution du langage et des idées d'une personne, un certain processus d'approximation successive est observé.

Dans le système moderne d'apprentissage automatique, la sommation des informations est beaucoup plus rapide. Imaginez que nous prenions toutes sortes d'objets à travers le monde et que nous les alimentions en fonctions FeatureSpacePlot pour voir ce qui se passe. Si nous obtenons certains clusters dans l'espace des fonctionnalités, nous pouvons conclure que chacun d'eux peut être défini comme correspondant à un certain «concept», qui, par exemple, peut être marqué avec un mot.

Honnêtement, ce qui arrive à FeatureSpacePlot - comme dans le processus de développement intellectuel humain - est, en un sens, un processus étape par étape. Pour distribuer des objets par espace d'entité, FeatureSpacePlot utilise des fonctions qu'il a apprises à extraire des tentatives précédentes de catégorisation.

Eh bien, si nous acceptons le monde tel qu'il est, quelles sont les meilleures catégories - ou concepts - qui peuvent être utilisées pour décrire les choses? Cette question est en constante évolution. En général, toutes les percées - qu'il s'agisse de science, de technologie ou d'autre chose - sont souvent précisément associées à la réalisation de la possibilité d'identifier une nouvelle catégorie ou un nouveau concept de manière utile.

Mais dans le processus d'évolution de notre civilisation, il y a une certaine spirale. Tout d'abord, un certain concept défini est défini - disons, l'idée d'un programme. Après cela, les gens commencent à l'utiliser et à réfléchir dans ses termes. Bientôt, de nombreux concepts différents sont construits sur la base de ce concept. Et puis un autre niveau d'abstraction est déterminé, de nouveaux concepts basés sur le précédent sont créés.

L'histoire est caractéristique de l'ensemble technologique de connaissances de la civilisation moderne et de son ensemble intellectuel de connaissances. Là et là, il y a des tours de concepts et des niveaux d'abstraction qui se succèdent.

Problème d'apprentissage

Pour que les gens puissent communiquer en utilisant un certain concept, ils doivent le savoir. Et, oui, certains concepts (comme la constance des objets) sont automatiquement reconnus par les gens simplement en observant la nature. Mais supposons que, si vous regardez la liste des mots courants de l'anglais moderne, il deviendra clair que la plupart des concepts utilisés par notre civilisation moderne ne s'appliquent pas à ceux que les gens connaissent d'eux-mêmes, observant la nature.

Au lieu de cela - qui rappelle beaucoup l'apprentissage automatique moderne - ils ont besoin d'une connaissance spéciale du monde "sous surveillance", organisée afin de souligner l'importance de certains concepts. Et dans des domaines plus abstraits (comme les mathématiques), ils ont probablement besoin de rencontrer des concepts sous leur forme abstraite immédiate.

Eh bien, mais aurons-nous besoin d'apprendre de plus en plus tout le temps avec l'augmentation de la quantité de connaissances intellectuelles accumulées de la civilisation? On peut craindre qu'à un moment donné, notre cerveau ne puisse tout simplement pas suivre le développement, et nous devrons ajouter une aide supplémentaire. Mais il me semble que c'est heureusement un de ces cas où le problème peut être résolu "au niveau logiciel".

Le problème est le suivant: à tout moment de l'histoire, il existe un certain ensemble de concepts qui sont importants pour la vie dans le monde à cette époque. Et, oui, avec le développement de la civilisation, de nouveaux concepts sont révélés et de nouveaux concepts sont introduits.Cependant, il existe un autre processus: les nouveaux concepts introduisent de nouveaux niveaux d'abstraction, comprenant généralement un grand nombre de concepts antérieurs.

Nous pouvons souvent observer cela dans la technologie. Il fut un temps où vous deviez connaître beaucoup de détails de bas niveau pour travailler sur un ordinateur. Mais au fil du temps, ces détails se sont résumés, alors maintenant vous n'avez besoin que d'un concept général. Vous cliquez sur l'icône et le processus démarre - vous n'avez pas besoin de comprendre les subtilités du fonctionnement des systèmes d'exploitation, des gestionnaires d'interruption, des planificateurs et tous les autres détails.

Et bien sûr, Wolfram Language en fournit un excellent exemple. Cela met beaucoup d'efforts à automatiser un grand nombre de détails de bas niveau (par exemple, lequel des algorithmes doit être utilisé) et permet aux utilisateurs de penser dans des concepts de haut niveau.

Oui, il faut toujours des gens qui comprennent les détails qui sous-tendent les abstractions (bien que je ne sais pas combien de tailleurs de pierre la société moderne a besoin). Mais pour la plupart, l'éducation peut se concentrer sur un haut niveau de connaissances.

On suppose souvent que pour atteindre des concepts de haut niveau dans le processus d'apprentissage, une personne doit d'abord résumer en quelque sorte l'histoire de la façon dont ces concepts sont devenus historiquement. Mais généralement - et, peut-être, toujours - il semble que ce ne soit pas le cas. Vous pouvez donner un exemple extrême: imaginez que pour apprendre à utiliser un ordinateur, vous devez d'abord parcourir toute l'histoire de la logique mathématique. Cependant, on sait en fait que les gens se tournent immédiatement vers les concepts modernes de l'informatique, sans avoir besoin d'étudier une sorte d'histoire.

Mais à quoi ressemble alors la clarté du réseau de concepts? Y a-t-il des concepts qui ne peuvent être compris qu'en comprenant d'autres concepts? Étant donné la formation des personnes sur la base de l'interaction avec l'environnement (ou la formation d'un réseau de neurones), leur ordre peut probablement exister.

Mais il me semble qu'un certain principe, similaire à l'universalité de l'informatique, suggère qu'avec un «cerveau pur» en main, on peut partir de n'importe où. Donc, si certains extraterrestres apprenaient la théorie des catégories et presque rien d'autre, ils construiraient, sans aucun doute, un réseau de concepts où cette théorie est à la racine, et ce que nous connaissons comme les bases de l'arithmétique serait étudié à partir d'eux quelque part dans l'analogue de notre institut.

Bien sûr, de tels extraterrestres pourraient construire leur ensemble de technologies et leur environnement d'une manière très différente de nous - tout comme notre histoire pourrait devenir complètement différente si les ordinateurs pouvaient être développés avec succès au 19ème siècle, et non au milieu du 20ème.

Progression mathématique

J'ai souvent réfléchi à la mesure dans laquelle la trajectoire historique des mathématiques est soumise au rôle du hasard et dans quelle mesure elle était inévitable. Comme je l'ai déjà mentionné, au niveau des systèmes formels, il existe de nombreux systèmes d'axiomes possibles sur lesquels vous pouvez construire quelque chose qui ressemble formellement aux mathématiques.

Mais la véritable histoire des mathématiques n'a pas commencé avec un système arbitraire d'axiomes. Il a commencé au temps des Babyloniens avec des tentatives d'utiliser l'arithmétique pour le commerce et la géométrie à des fins d'aménagement du territoire. Et à partir de ces racines pratiques, des niveaux d'abstraction ont commencé à s'ajouter, ce qui a finalement conduit aux mathématiques modernes - par exemple, les nombres ont été progressivement généralisés des entiers positifs au rationnel, puis aux racines, puis à tous les entiers, aux fractions décimales, aux nombres complexes, à l' algèbre nombres, aux quaternions , etc.

Y a-t-il une fatalité d'une telle voie de développement des abstractions? Je soupçonne, dans une certaine mesure, oui. C'est peut-être le cas avec d'autres types de formation de concepts. Ayant atteint un certain niveau, vous avez la possibilité d'étudier diverses choses, et au fil du temps, des groupes de ces choses deviennent des exemples de constructions plus générales et abstraites - qui à leur tour déterminent un nouveau niveau, à partir duquel, on peut apprendre quelque chose de nouveau.

Existe-t-il des moyens de sortir de ce cycle? Une possibilité peut être liée aux expériences mathématiques. On peut systématiquement prouver des choses liées à certains systèmes mathématiques. Mais on peut empiriquement juste remarquer des faits mathématiques - comme Ramanujan une fois remarqué que $$$e^{\pi \sqrt{163}}$



De la même manière que l'on peut numéroter les systèmes axiomatiques, on peut imaginer la numérotation des questions possibles en mathématiques. Mais cela pose immédiatement un problème. Le théorème de Gödel déclare que dans des systèmes d'axiomes tels que ceux liés à l'arithmétique, il existe des théorèmes «formellement insolubles» qui ne peuvent pas être prouvés ou réfutés dans le cadre de ce système d'axiomes.

Cependant, les exemples spécifiques créés par Gödel semblaient très loin de ce qui pouvait réellement se produire dans les cours de mathématiques. Et pendant longtemps, on a cru que le phénomène d'insolvabilité était en quelque sorte quelque chose qui, en principe, existe, mais ne sera pas lié aux «mathématiques réelles».

Cependant, selon mon principe d'équivalence informatique et mon expérience dans l'univers informatique, je suis à peu près sûr que ce n'est pas le cas - et qu'en fait, l'insolvabilité est très proche même en mathématiques typiques. Je ne serais pas surpris qu'une partie tangible des problèmes de mathématiques non résolus aujourd'hui ( hypothèse de Riemann , P = NP, etc.) soit insoluble.

Mais s'il y a beaucoup d'insolvabilité, comment se fait-il que tant de choses en mathématiques soient résolues avec succès? Je pense que c'est parce que les problèmes résolus avec succès ont été spécialement choisis pour éviter l'insolvabilité, simplement en raison de la façon dont le développement des mathématiques est construit. Parce que si, en fait, nous formons des niveaux d'abstraction successifs sur la base de concepts que nous avons prouvés, alors nous ouvrons la voie qui peut aller de l'avant sans se transformer en insolubilité.

Bien sûr, les mathématiques expérimentales ou les «questions aléatoires» peuvent immédiatement nous conduire à un domaine plein d'insolvabilité. Mais, du moins pour l'instant, la discipline de base des mathématiques ne s'est pas développée de cette façon.

Et qu'en est-il de ces "faits aléatoires des mathématiques"? Oui, comme pour les autres domaines de recherche intellectuelle. Les «faits aléatoires» ne sont pas inclus dans la voie du développement intellectuel tant qu'une structure - généralement quelques concepts abstraits - n'est pas construite autour d'eux.

Un bon exemple est ma découverte préférée de l'origine de la complexité dans de tels systèmes, généralement 30 automates cellulaires. Oui, des phénomènes similaires ont déjà été observés il y a même des milliers d'années (par exemple, le hasard dans une séquence de nombres premiers). Mais sans une plate-forme conceptuelle plus large, peu de gens y ont prêté attention.

Un autre exemple est celui des séquences imbriquées (fractales). Il y a quelques exemples de la façon dont ils se sont rencontrés dans la mosaïque du XIIIe siècle, mais personne n'y a prêté attention jusqu'à ce que dans les années 1980 une plate-forme entière apparaisse autour des fractales.

La même histoire se répète encore et encore: tant que les concepts abstraits ne sont pas définis, il est difficile de parler de nouveaux concepts, même face à un phénomène qui les démontre.

Je soupçonne que c'est le cas en mathématiques: il y a une certaine superposition inévitable de certains concepts abstraits au-dessus d'autres, qui détermine le chemin des mathématiques. Cette façon est-elle unique? Sans doute, non. Dans le vaste espace des faits mathématiques possibles, certaines directions sont choisies pour d'autres constructions. Mais vous pouvez en choisir d'autres.

Est-ce à dire que les sujets en mathématiques sont inévitablement entraînés par des accidents historiques? Pas autant qu'on pourrait le penser. En effet, comme les mathématiques ont été découvertes à maintes reprises, en commençant par des choses comme l'algèbre et la géométrie, il existe une tendance remarquable dans laquelle différentes directions et différentes approches conduisent à des résultats équivalents ou correspondant les uns aux autres.

Peut-être, dans une certaine mesure, cela est une conséquence du principe d'équivalence informatique et du phénomène d'universalité informatique: bien que les règles de base (ou «langage») utilisées dans différents domaines des mathématiques diffèrent, le résultat est un moyen de traduire entre elles - et au niveau suivant d'abstraction. le chemin choisi ne sera plus aussi critique.

Preuve logique et automatisation de l'abstraction

Revenons aux preuves logiques. Comment sont-ils liés aux mathématiques typiques? Jusqu'à présent, aucun moyen. Oui, la preuve a nominalement la même forme que la preuve mathématique standard. Mais ce n'est pas "convivial pour les maths". Ce ne sont que des pièces mécaniques. Il n'est pas associé à des concepts abstraits de haut niveau qui seront compréhensibles par les mathématiques humaines.

Cela nous aiderait beaucoup si nous trouvions que des lemmes de preuve non triviaux sont déjà apparus dans la littérature mathématique (je ne pense pas, mais nos possibilités de recherche par théorèmes n’ont pas encore atteint un niveau tel que nous pouvons en être sûrs). Mais s'ils apparaissent, cela nous donnera probablement un moyen de relier ces lemmes à d'autres choses en mathématiques et de définir leur cercle de concepts abstraits.

Mais comment rendre les preuves explicables sans cela?

Peut-être existe-t-il une autre manière de réaliser la preuve, fondamentalement plus fortement liée aux mathématiques existantes. Mais même avec les preuves que nous avons maintenant, on peut imaginer «peaufiner» de nouveaux concepts qui définiraient un niveau d'abstraction plus élevé et placeraient cette preuve dans un contexte plus général.

Je ne sais pas comment faire ça. J'envisageais de proposer un prix (quelque chose comme mon prix Turing 2007) pour «transformer des preuves en une forme compréhensible». Cependant, il est totalement incompréhensible de savoir comment évaluer «l'explicabilité». On pourrait être invité à enregistrer une vidéo d'une heure dans laquelle une explication réussie de la preuve serait donnée, adaptée à un mathématicien typique - mais ce serait très subjectif.

Mais de la même manière qu'il est possible d'automatiser la recherche de belles dispositions de réseaux, nous pouvons peut-être automatiser le processus de transformation des preuves en explicables. La preuve actuelle, en fait, sans explication, suggère de considérer plusieurs centaines de lemmes. Mais supposons que nous puissions définir un petit nombre de lemmes «intéressants». Peut-être pourrions-nous en quelque sorte les ajouter à notre canon des mathématiques célèbres, puis nous pourrions les utiliser pour comprendre la preuve.

Il y a une analogie avec le développement des langues. En créant le Wolfram Language, j'essaie d'identifier les «morceaux de travail informatique» dont les gens ont souvent besoin. Nous créons à partir d'eux des fonctions intégrées dans le langage, avec des noms spécifiques que les gens peuvent utiliser pour s'y référer.

Un processus similaire est en cours - bien que pas du tout organisé de la sorte - dans l'évolution des langues naturelles. Les «morceaux de sens» qui se révèlent utiles finissent par faire passer leurs mots dans la langue. Parfois, ils commencent par des phrases composées de plusieurs mots existants. Mais les plus influents s'avèrent généralement si éloignés des mots existants qu'ils apparaissent sous forme de nouveaux mots, qui sont potentiellement assez difficiles à définir.

Dans le développement de la langue Wolfram, dont les fonctions sont appelées à l'aide de mots anglais, je me fie à la compréhension générale de la langue anglaise par une personne (et parfois à la compréhension des mots utilisés dans les applications informatiques courantes).

Il faudrait faire quelque chose de similaire pour déterminer quels lemmes ajouter au canon mathématique. Il faudrait non seulement s'assurer que chaque lemme serait en quelque sorte «essentiellement intéressant», mais aussi sélectionner des lemmes «faciles à déduire» des concepts et résultats mathématiques existants.

Mais qu'est-ce qui rend le lemme «essentiellement intéressant»? Il faut dire qu'avant de travailler sur mon livre, j'ai blâmé le choix des lemmes (ou tours) dans n'importe quel domaine des mathématiques décrit et nommé dans les manuels, le grand arbitraire et les accidents historiques.

Mais, après avoir analysé en détail les théorèmes de la logique de base, j'ai été surpris de trouver quelque chose de complètement différent. Supposons que nous avons construit tous les théorèmes corrects de la logique dans l'ordre de leur taille
(par exemple, p = p sera le premier, p ET p = p - un peu plus tard, etc.). Cette liste a beaucoup de redondance. La plupart des théorèmes s'avèrent être une extension triviale des théorèmes qui sont déjà apparus sur la liste.

Mais parfois, un théorème apparaît qui produit de nouvelles informations qui ne peuvent pas être prouvées sur la base de théorèmes qui sont déjà apparus sur la liste. Un fait remarquable: il existe 14 de ces théorèmes , et ils correspondent, en substance, exactement aux théorèmes qui sont généralement donnés des noms dans les manuels de logique (ici ET est ∧, OU est ∨, et PAS est ¬.)


En d'autres termes, dans ce cas, les théorèmes nommés ou «intéressants» sont précisément ceux qui font des déclarations sur de nouvelles informations d'une taille minimale. Oui, selon cette définition, après un certain temps, de nouvelles informations n'existeront plus, car nous obtiendrons tous les axiomes nécessaires pour prouver tout ce qui est possible - bien que vous puissiez aller plus loin en commençant à limiter la complexité des preuves admissibles.

Qu'en est-il des théorèmes NAND, par exemple, ceux trouvés dans la preuve? Encore une fois, vous pouvez construire tous les vrais théorèmes dans l'ordre, et trouver ceux qui ne peuvent pas être prouvés sur la base des théorèmes précédents de la liste:


NAND n'a pas de tradition historique comme ET, OU et NON. Et, apparemment, il n'y a pas de langage humain dans lequel NAND est désigné par un mot. Mais dans la liste des théorèmes NAND, le premier des précédents est facilement reconnu comme commutativité de NAND. Après cela, seules quelques traductions sont nécessaires pour leur donner des noms: a = (a · a) · (a · a) est comme la double négation, a = (a · a) · (a · b) est comme la loi d'absorption , (a · A) · b = (a · b) · b est similaire à "l'affaiblissement", et ainsi de suite.

Eh bien, si nous allons apprendre quelques «théorèmes clés» de la logique NAND, quel genre de théorèmes devraient-ils être? Peut-être que ce devraient être des «lemmes populaires» dans les épreuves.

Bien sûr, tout théorème peut avoir de nombreuses preuves possibles. Mais supposons que nous n'utilisions que les preuves produites par FindEquationalProof. Il s'avère ensuite que dans la preuve des mille premiers théorèmes NAND, le lemme le plus populaire est a · a = a · ((a · a) · a), suivi de lemmes du type (a · (((a · a) · a)) · ( a (a ((a a) a))) = a.

Quels sont ces lemmes? Ils sont utiles pour les méthodes utilisées par FindEquationalProof. Mais pour les gens, ils ne semblent pas très adaptés.

Qu'en est-il des lemmes qui se révèlent courts? a · b = b · a n'est certainement pas le plus populaire, mais le plus court. (a · a) · (a · a) = a est plus populaire, mais plus long. Et puis il y a des lemmes tels que (a · a) · (b · a) = a.

Quelle sera l'utilité de ces lemmes? Voici une façon de vérifier cela. Examinons les mille premiers théorèmes NAND et évaluons comment l'ajout de lemmes raccourcit les preuves de ces théorèmes (au moins celles trouvées par FindEquationalProof):


a · b = b · a est très efficace et coupe souvent la preuve de près de 100 étapes. (a · a) · (a · a) = a a beaucoup moins de succès; il «confond parfois» FindEquationalProof, vous forçant à prendre plus de mesures que nécessaire (valeurs négatives sur les graphiques). (a · a) · (b · a) = a résiste bien à la contraction, mais pas aussi bien que a · b = b · a. Cependant, si vous le combinez avec a · b = b · a, par conséquent, les réductions se produisent plus souvent.

L'analyse peut être poursuivie, par exemple, en incluant une comparaison de la mesure dans laquelle un lemme particulier raccourcit la longueur des preuves par rapport à leur longueur d'origine. Mais le problème est que si vous ajoutez quelques "lemmes utiles" comme a · b = b · a et (a · a) · (b · a) = a, il y a encore beaucoup de preuves longues - c'est-à-dire, beaucoup de ce qui est nécessaire Pour comprendre.

Que pouvons-nous comprendre?

Il existe différentes façons de modéliser les choses. Pendant plusieurs centaines d'années, les sciences exactes ont été dominées par l'idée de trouver des équations mathématiques qui pourraient être résolues pour montrer comment le système se comporterait. Mais depuis l'avènement de mon livre, il y a eu un changement actif vers la création de programmes que vous pouvez exécuter pour voir comment les systèmes vont se comporter.

Parfois, ces programmes sont écrits pour une tâche spécifique; parfois, ils sont recherchés depuis longtemps. Et à notre époque, au moins une classe de ces programmes est dérivée en utilisant l'apprentissage automatique, par la méthode du mouvement inverse à partir d'exemples connus de comportement du système.

Et est-il facile de «comprendre ce qui se passe» avec ces différents types de modélisation? Trouver la «solution exacte» des équations mathématiques est un gros plus - alors le comportement du système peut être décrit par une formule mathématique exacte. Mais même lorsque ce n'est pas le cas, il est souvent possible d'écrire quelques énoncés mathématiques suffisamment abstraits pour être liés à d'autres systèmes et comportements.

Comme je l'ai écrit ci-dessus, avec un programme - comme un automate cellulaire - tout peut être différent. Très souvent, il arrive que nous rencontrons immédiatement une irréductibilité informatique, ce qui limite notre capacité à aller un peu plus loin et à «expliquer» ce qui se passe.

Qu'en est-il de l'apprentissage automatique et des réseaux de neurones? En un sens, la formation au réseau neuronal est comme un bref résumé de la recherche inductive en cours dans les sciences naturelles. Nous essayons, à partir d'exemples, de déduire un modèle de comportement du système. Mais sera-t-il alors possible de comprendre le modèle?

Et encore une fois, il y a des problèmes d'irréductibilité informatique. Mais discutons d'un cas dans lequel nous pouvons imaginer à quoi ressemblerait la situation dans lequel nous pouvons comprendre ce qui se passe.

Au lieu d'utiliser un réseau de neurones pour simuler le comportement du système, examinons la création d'un réseau de neurones qui classe certains aspects du monde: par exemple, prendre des images et les distribuer en fonction de leur contenu («bateau», «girafe», etc.). Lorsque nous formons le réseau neuronal, il apprend à produire la sortie correcte. Mais vous pouvez potentiellement imaginer ce processus comme une construction interne d'une séquence de différences (quelque chose comme un jeu de " vingt questions "), qui détermine finalement la conclusion correcte.

Mais quelles sont ces différences? Parfois, nous pouvons les reconnaître. Par exemple, "Y a-t-il beaucoup de bleu dans l'image?" Mais la plupart du temps, ce sont des propriétés du monde que les gens ne remarquent pas. Peut-être existe-t-il une histoire alternative des sciences naturelles dans laquelle certaines d'entre elles se révéleraient. Mais ils ne font pas partie du canon actuel de la perception ou de l'analyse.

Si nous voulions les ajouter, nous pourrions peut-être trouver des noms pour eux. Mais cette situation est similaire à la situation avec des preuves logiques. Le système automatique a créé certaines choses qu'il utilise comme jalons pour générer le résultat. Mais nous ne reconnaissons pas ces jalons, ils ne signifient rien pour nous.

Encore une fois, si nous avons constaté que certaines différences spécifiques se retrouvent souvent dans les réseaux de neurones, nous pourrions décider qu'elles méritent d'être étudiées par nous-mêmes et les ajouter au canon standard des façons de décrire le monde.

Pouvons-nous nous attendre à ce qu'un petit nombre de ces différences nous permettent de créer quelque chose de significatif? Il semble que la question soit de savoir si un petit nombre de théorèmes nous aidera à comprendre une telle chose comme preuve logique.

Je pense que la réponse n'est pas claire. Si vous étudiez, par exemple, un grand nombre d'ouvrages scientifiques en mathématiques, vous pouvez poser des questions sur la fréquence d'utilisation de divers théorèmes. Il s'avère que la fréquence des théorèmes correspond presque parfaitement à la loi de Zipf (et en premier lieu il y aura un théorème central limite ,théorème de fonction implicite et théorème de Tonelli-Fubini ). La même chose se produit probablement avec des différences qui «valent la peine d'être connues», ou avec de nouveaux théorèmes qui «valent la peine d'être connus».

La connaissance de plusieurs théorèmes nous donnera l'opportunité d'avancer assez loin, mais il y aura toujours une queue exponentielle infinie, et nous n'arriverons pas à la fin.

L'avenir de la connaissance

En étudiant les mathématiques, la science ou la technologie, vous pouvez voir des voies de base similaires de développement qualitatif, consistant à construire un ensemble d'abstractions toujours croissantes. Ce serait bien de quantifier ce processus. Il est peut-être possible de calculer comment certains termes ou descriptions qui se trouvent souvent en même temps sont inclus dans des niveaux d'abstraction plus élevés, auxquels de nouveaux termes ou descriptions apparaissent à leur tour en relation avec eux.

Il peut être possible de créer un modèle idéalisé de ce processus en utilisant un modèle formel de calcul tel que les machines de Turing. Imaginez qu'au niveau le plus bas, il y ait une machine de Turing de base sans abstractions. Imaginez maintenant que nous sélectionnions des programmes pour cette machine de Turing selon un processus aléatoire spécifique. Ensuite, nous exécutons ces programmes et les analysons pour voir quel modèle du niveau de calcul "supérieur" peut reproduire avec succès le comportement conjoint de ces programmes sans avoir à effectuer chaque étape de chacun d'eux.

Il pourrait être décidé que l'irréductibilité du calcul conduirait au fait que la création de ce modèle de calcul de niveau supérieur serait inévitablement plus compliquée. Mais le point clé est que nous essayons seulement de reproduire le comportement commun des programmes, et non leur comportement séparé.

Mais que se passe-t-il si ce processus se répète encore et encore, reproduisant l'histoire intellectuelle idéalisée de l'homme et créant une tour d'abstractions toujours plus élevée?

Vraisemblablement, nous pouvons ici faire une analogie avec les phénomènes critiques en physique et la méthode du groupe de renormalisation . Si c'est le cas, nous pouvons imaginer que nous pouvons déterminer la trajectoire dans l'espace des plates-formes pour représenter les concepts. Que fera cette trajectoire?

Peut-être aura-t-il une valeur fixe quand, à n'importe quel moment de l'histoire, il y aura à peu près autant d'études valables sur les concepts - de nouveaux concepts s'ouvriront lentement et les anciens seront absorbés.

Qu'est-ce que cela signifie pour les mathématiques? Par exemple, que tout «fait mathématique aléatoire» découvert empiriquement sera finalement considéré lorsqu’il atteindra un certain niveau d’abstraction. Il n'y a pas de compréhension évidente du fonctionnement de ce processus. En effet, à tout niveau d'abstraction, il y a toujours de nouveaux faits empiriques auxquels il faut "sauter". Il peut également arriver que «l'élévation du niveau d'abstraction» se déplace plus lentement que nécessaire pour ces «sauts».

L'avenir de la compréhension

Qu'est-ce que tout cela signifie pour la compréhension future?

Dans le passé, lorsque les gens étudiaient la nature, ils avaient un petit nombre de raisons pour la comprendre. Parfois, ils en personnifiaient certains aspects sous la forme d'esprits ou de divinités. Mais ils l'ont accepté tel quel, sans penser à la possibilité de comprendre tous les détails des causes des processus.

Avec l'avènement de la science moderne - et surtout quand de plus en plus de nos vies sont passées dans des environnements artificiels dominés par les technologies développées par nous - ces attentes ont changé. Et lorsque nous étudions les calculs effectués par l'IA, nous n'aimons pas que nous ne les comprenions pas.

Cependant, il y aura toujours une compétition entre ce que font les systèmes de notre monde et ce que notre cerveau peut calculer à partir de leur comportement. Si nous décidons d'interagir uniquement avec des systèmes beaucoup plus simples que le cerveau en puissance de calcul, alors nous pouvons nous attendre à pouvoir comprendre systématiquement ce qu'ils font.

Mais si nous voulons utiliser toutes les capacités informatiques disponibles dans l'univers, alors inévitablement, les systèmes avec lesquels nous interagissons atteindront la puissance de traitement de notre cerveau. Et cela signifie que, selon le principe de l'irréductibilité informatique, nous ne pouvons jamais systématiquement «dépasser» ou «comprendre» le fonctionnement de ces systèmes.

Mais comment alors les utiliser? Eh bien, tout comme les humains ont toujours utilisé les systèmes de la nature. Bien sûr, nous ne connaissons pas tous les détails de leur travail ou de leurs capacités. Mais à un certain niveau d'abstraction, nous en savons assez pour comprendre comment atteindre nos objectifs avec leur aide.

Qu'en est-il des domaines comme les mathématiques? En mathématiques, nous sommes habitués à construire notre ensemble de connaissances afin de pouvoir comprendre chaque étape. Mais les mathématiques expérimentales - ainsi que des fonctionnalités telles que la preuve automatique des théorèmes - mettent en évidence l'existence de domaines dans lesquels une telle méthode ne sera pas disponible pour nous.

Les appellerons-nous «mathématiques»? Je pense qu'ils devraient. Mais cette tradition est différente de celle à laquelle nous sommes habitués au cours du dernier millénaire. Nous pouvons encore y créer des abstractions et construire de nouveaux niveaux de compréhension.

Mais quelque part dans sa base, il y aura toutes sortes de versions différentes de l'irréductibilité informatique, que nous ne pourrons jamais transférer dans le domaine de la compréhension humaine. C'est à peu près ce qui se passe dans la preuve de mon petit axiome de logique. Ceci est un exemple précoce de ce que je pense être l'un des principaux aspects des mathématiques - et bien plus - à l'avenir.