En 1932, Alonzo Church (maître spirituel d'Alan Turing, un des clèbres père fondateur de l'Intelligence artificielle) invente le lambda calcul, un langage logique de bas niveau. Ce langage permet de décrire, à l'aide trois opérations seulement, pratiquement l'ensemble des mathématiques. (plus de précisions, si vous en souhaitez, seront données)

Dans les années 50, les informaticiens se rendent compte que ce langage est parfait pour l'ordinateur : sa syntaxe simpliste permet de décrire les programmes et leurs opérations dans un langage légèrement plus complexe que le langage (binaire). Il est parfait pour la programmation.

Quelques années plus tard, les mathématiciens de l'époque découvrent la puissance descriptive du lambda calcul, qui permet également de décrire les mathématiques...

1997 : Jean-Louis krivine démontre que le lambda calcul permet en fait d'exprimer tous les raisonnements possibles et imaginables, et conséquemment, toutes les structures mathématiques connues.

Dès lors, ce langage devient universel, et devient également une Pierre de rosette Mathématiques : on décrit des formules d'un langage informatique en lambda calcul, puis on retraduit la traduction en langage mathématiques... Un algorithme informatique devient une formule mathématique. Vous ne voyez pas encore la puissance de cette constatation...

Imaginez un langage, ou de nombreuses choses sont démontrées. Ce langage a permis la constitution d'une immense base de connaissance, mais celle-ci reste limitée. on ne peut l'utiliser qu'avec le langage sus-dit. Grâce au lambda calcul, on peut traduire les vérités d'une base de connaissance propre à un langage, dans un autre. C'est ce qu'a fait le mathématicien français : en traduisant des programmes déjà existant, il a pu trouver des théorèmes, des structures mathématiques, qui n'avait jamais été découvertes par les mathématiciens. A l'inverse, traduire un théorème ou un corrolaire, en langage informatique, donne accès à un programme inconnu jusqu'alors... mais déjà existant, sous forme mathématique, donc démontré et fonctionnel...

Mais cela ne s'arrête pas là. Au rang des système de logique, le neurone se pose là : il s'agit d'un système binaire, après tout. Je m'allume, je ne m'allume pas... Avant d'aller plus loin, je vais vous parler d'un théorème formidable, véritable bombe mathématique en son temps, et dont on n'a pas fini de s'étonner : Le théorème d'incomplétude de Kurt Gödel. Il méritera plus tard un topic à lui tout seul... Ce théorème indique, en gros, que tout système mathématique suffisamment général, et donc puissant, se retrouve incompétent à se décrire lui même. Autrement dit, il existera tujours des vérités que les mathématiques seront incapables de démontrer, et ceci, est prouvé mathématiquement...

Ce théorème, traduit en lambda calcul, puis retraduit en langage informatique, donne des lignes de codes assez remarquables... Le programme obtenu à partir de ce théorème ressemble à s'y méprendre au petit programme servant à restaurer les données en cours d'utilisation, lorsque l'ordinateur s'est éteint brusquement : retrouver, parcourir toutes les données antérieurement en cours d'utilisation, puis restaurer celles qui ont subit des dommages...

Le théorème de Gödel, dieu sait par quel miracle (bien, en fait, ce n'en est pas réellement un ^^) décrit très justement le programme de sauvegarde de donnée, inventé depuis belle lurette, mais jamais en référence avec une certaine théorie de l'incomplétude... Plus fort encore... le cerveau a-t-il un langage traductible en lambda calcul? une constatation :

Parcourir les données, les lires, restaurer certaines...
Revivre les éléments de la journée, revivre les apprentissage et le vécu de la veille, reconsolider ces apprentissages...

Et oui! selon J-L Krivine, le théorème d'incomplétude serait une formulation mathématique de nos rèves...

Et ce n'est qu'un exemple... de nombreux programmes ont pu être trouvés par la simple traduction de formules mathématiques.. Inversement, de nombreux théorèmes mathématiques ont pu être démontré ou même découvert, grâce à la traduction de programmes informatiques... Tout cela pourrait bien être des traductions en langage mathématiques, ou informatiques, de phénomènes de la pensée... Après tout, ces théorèmes et programmes ne viennent bien que d'un endroit, le cerveau de l'homme...

Sources : diverses dont plusieurs articles de Jean-Louis Krivine