Les ordinateurs biomoléculaires, faits d'ADN et d'autres molécules biologiques, existent aujourd'hui seulement dans quelques laboratoires spécialisés. Néanmoins, Tom Ran et Shai Kaplan, deux étudiants qui développent leur recherche dans le laboratoire du Professeur Ehud Shapiro de l'Institut de Chimie Biologique, d'Informatique et de Mathématiques Appliquées ont trouvé une façon de rendre ces dispositifs microscopiques de calcul "conviviaux" en exécutant des calculs complexes et en répondant à des questions compliquées, comme rapporté dans l'article publié en ligne dans Nature Nanotechnology.

Shapiro et son équipe avaient déjà découvert en 2001 les 1ers ordinateurs à ADN programmables et autonomes, si petits qu'un milliard de ces systèmes est contenu dans une goutte d'eau. Trois ans plus tard, une nouvelle version de ces systèmes pouvait détecter des cellules cancéreuses dans une éprouvette et les détruire. En plus de pouvoir imaginer qu'un jour de tels dispositifs pourront être utilisés chez l'être humain, tels des nano-docteurs pouvant localiser et soigner les maladies, ces ordinateurs d'ADN pourront effectuer des millions de calculs en parallèle.

L'ordinateur biomoléculaire développé aujourd'hui suit la logique suivante : il est programmé avec une règle telle que "Tous les hommes sont mortels" et un fait tel que "Socrate est un homme". Lorsque l'on demande alors à l'ordinateur si Socrate est mortel, il répond correctement dans tous les cas. Parallèlement, l'équipe a développé un programme permettant la communication entre le langage de programmation classique d'un ordinateur et le code de fonctionnement de l'ordinateur à ADN. Pour parvenir à la réponse, différents brins d'ADN correspondants aux règles, faits et questions sont assemblés selon un processus hiérarchique par un système robotisé. Afin de visualiser la solution, des molécules naturellement fluorescentes ont été greffées sur certains brins d'ADN, avec une seconde protéine masquant l'émission de lumière. Une enzyme spécialisée est alors attirée sur le site de la réponse correcte, et "découvre" la molécule fluorescente, permettant ainsi la visualisation de la réponse.

Les ordinateurs biomoléculaires contenus dans ces gouttes d'eau ont pu ainsi répondre à des questions bien plus complexes en combinant différents fluorophores.

http://www.bulletins-electroniques.com/actualites/60785.htm

Trois jours de stage et six heures de train pendant lesquelles j'ai dévoré ce livre. Gilles Dowek a reçu le Grand Prix de Philosophie 2007 décerné par l'Académie Française. Je ne connais pas les autres lauréats mais pour ce qui est de ce livre je pense que la philosophie a vraiment trouvé du grain à moudre pour quelques années dans ces métamorphoses numériques.

Au début du livre, j'étais en territoire connu mais j'ai déjà lu beaucoup de livres sur l'histoire des mathématiques alors j'ai pensé, tiens encore une histoire des maths. C'est vrai pour le tout début du livre mais la première partie est nécessaire à quiconque ne maîtrise par bien ce sujet afin d'introduire la logique des prédicats.

Et puis dès la cinquantième page, je vois apparaître mon copain Kant et ses jugements synthétiques à priori. Alors je commence à me dire que ça va cogner. On pourra d'ailleurs lire le documents suivant : La philosophie des mathématiques de Kant . Quel est le problème?

Kant propose deux types de jugements :

Analytique si une proposition est vraie par définition comme "un triangle à trois cotés".

Synthétique si la propostion est vraie sans que ce soit une définition. Par exemple "La terre a un satellite" . Ce jugement peut être a priori si on peut le concevoir dans la tête ou a poseriori s'il faut une intéraction avec la nature.

Les jugements analytiques semblent quant à eux exclusivement à priori.

Pour Kant le raisonnement se situe dans les jugements synthétiques à priori mais c'est là que ça coince par ce que ce n'est pas aussi simple que ça!

Le "simple", 2+2=4 pose problème. Frege va d'ailleurs montrer que 2+2=4 peut se déduire de la définition des nombres entiers et doit être classé parmi les jugements analytiques et non parmi les jugements synthétiques à priori.

On voit déjà poindre à l'horizon une problématique philosophique centrale concernant les mathématiques, leur constitution et leur évolution. Se constituent-elles au sein d'elles mêmes auquelles cas elles sont analytiques à partir des simples définitions. Relèvent-elles du jugement synthétique à priori ou doivent-elles aller chercher des éléments dans la nature pour se construire.

Il est inutile de vouloir répondre simplement à ces questions qui dépendent de l'évolution des mathématiques elles mêmes dont le pivot central est certainement la thèse de Church des années 30, affirmant l'identité entre la notion de calcul "informatique et la notion "commune " de calcul que nous avons.

En avançant encore un peu dans le livre on voit apparaitre l'idée selon laquelle Démonstration = Algorithme et puisque la thèse de Church nous donne Algorithme = Calcul, on a donc l'identité Démonstration = Calcul. Il devient donc nécessaire de distinguer les notions de démontrable et d'explicatif, ce qui est loin d'être facile pour les mathématiciens. La longueur des démonstrations est aussi abordée, avec par exemple la problèmatique suivante : Peut-on démontrer qu'un problème démontrable possède une démonstration "courte"?

Philosophiquement le sujet est dense!

D'autant qu'à la fin de l'histoire une surprise de taille nous attend avec un retour nécessaire à la nature... Mais je n'en dis pas plus.

Ce qui m'a aussi passioné dans le livre est le traitement du rapport du mathématicien et de la machine, de ce nouvel outil qui lui est maintenant indispensable. L'auteur s'interroge aussi sur le fait que l'ordinateur du mathématicien est le même que celui de Mme Michu, sauf bien sûr si les calculs sont vraiment très très longs et demandent un super-calculateur pour pouvoir être faits  en un temps "raisonnable". Il est intreressant de comprendre quelles est la place de l'ordinateur-machine à coté du mathématicien-humain.

J'ai extrait quelques courtes citations vers la fin du livre qui me semblent assez explicites sur les métamorphoses du calcul qui est le sujet du livre et donc des mathématiques elles-mêmes:

En 1976, les mathématiques sont entrées dans la période instrumentée de leur histoire. Les instruments utilisés par les mathématiciens, ne sont pas des instruments qui prolongent les facultés de nos sens, mais qui prolongent les capacités de notre entendement: notre faculté de raisonner et surtout, de calculer. ( p 182 )

L'utilisation d'instruments commence, de même à changer, les mathématiques. ( p 182 )

La maquette sur laquelle on fait l'essai est donc une machine à résoudre un problème mathématique,[...] (p 188)

L'entrée des mathématiques dans leur ère instrumentée incite donc, non à accorder une confiance excessive dans les instruments utilisés, mais à restreindre prudemment la confiance parfois exagérée, que nous avons en nous-mêmes: nous aussi nous pouvons faire des erreurs. (  p 191 )

Podcast de Gille Dowek sur le livre et sur Canal-Académie

Pour compléter :

Des p'tits problèmes de coloriage ( autour du théorème des quatre couleurs)

Comment les mathématiciens prouvent-t-il un théorème ?

Lorsqu'ils le prouvent d'une façon traditionnelle, ils présentent les arguments les uns à la suite des autres, comme un récit. Ils s'appuient sur des résultats précédemment démontrés ( par eux ou par d'autres), ils cachent les détails dont ils sont certains que les experts qui les liront n'auront pas besoin pour les comprendre, ils prennent des raccourcis pour rendre la lecture moins ennuyeuse. 
La validité des arguments avancés est accordée après un examen minitieux par d'autres mathématiciens de la longue ( très longue parfois ) preuve ou au cours de discussions informelles, lors de séminaires, de cours ou après publication dans des revues spécialisées.
Lorsque ces experts parviennent au coeur de la démonstration, ils affinent la lecture et généralement les erreurs qui ont pu se glisser dans la démonstration sont trouvées. Cependant l'histoire des mathématiques n'est pas exempte d'exemple où il a été mis un temps très important pour que la communauté mathématique découvre une erreur ou un résultat faux. De plus, dans quelques cas récents, la lecture des preuves a été particulièrement longue et compliquée, d'autant plus que maintenant de plus en plus de preuves utilisent du code informatique.

Comment les mathématiciens peuvent-ils être sûrs que de telles preuves sont fiables ?

De façon habituelle, les mathématiciens, s'ils ne savent pas résoudre un problème, le ramènent à un problème qu'ils savent résoudre. S'ils ne peuvent plus faire de démonstration à la main, il suffit qu'ils fassent faire à l'ordinateur ce qu'ils faisaient usuellement à la main. Mathématiciens et informaticiens  ont donc commencé à développer le vaste champ de la preuve formelle. La preuve formelle nécessite la vérification de chaque inférence à partir des axiomes de départ. Si les mathématiciens ne produisaient auparavant aucune preuve dans un langage formel, c'est qu'il aurait été impossible de la faire lire par la communauté mathématique, mais maintenant qu'un ordinateur peut lire et valider une preuve, il risque d'en être autrement. Les avancées dans la preuve formelle sont telles qu'il est maintenant possible de l'utiliser pour des tâches difficiles.

Mais jusqu'où iront-ils ?

Si les ordinateurs ( aidés par les mathématiciens et les informaticiens ! ) sont maintenant capables de se lancer dans les démonstrations, ils sont aussi en mesure de se lancer dans l'exploration des mathématiques elles-mêmes et d'émettre des conjectures ( hypothèses pour les autres disciplines). On peut ainsi les laisser chercher quelques relations qui n'auraient pas été vues par l'oeil du mathématicien. Les mathématiciens peuvent aussi se lancer dans l'observation des ordinateurs qui parcourent les mathématiques et apprendre ainsi de nouvelles choses. Il s'agirait d'un changement profond dans la façon de concevoir les mathématiques et de les faire. Un rêve serait d'ailleurs de voir les ordinateurs en mesure de valider toutes les preuves des théorèmes fondamentaux, activité qui s'apparenterait au séquencement du génome mathématique.

La source en anglais Science Daily

Un mathématicien post-moderne

En des temps bien reculés, il fût décidé par Reine Démocratie que Dame Politique s'occuperait exclusivement de l'organisation de la Cité et de son administration. C'est ainsi que Politique s'engageait dans des conversations longues et difficiles pour s'accorder avec ses soeurs des Cités voisines de la taille de chacune des dites Cités, et  de leurs droits associés. Ceci déclencha moultes guerres. Pendant ce temps les commerçants vendaient et achetaient, suivant le temps qu'il faisait chez Dame Politique. Ils eurent d'ailleurs l'idée géniale pour augmenter leurs transactions de vendre de l'argent! Pour cela ils firent appel à Dame Mathématique. Elle leur rendit bien des services pour organiser ce marché autoréférent. Mais l'autoréférence est vraiment le cheval de bataille de Dame Mathématique. Son histoire est parsemée des paradoxes que l'autoréférence n'a cessé de semer sous ses pieds. Dame Mathématique eut l'idée d'estimer le prix de l'argent à l'aide du taux d'intérêt. De longs débats s'en suivirent pour le fixer et trouver les mécanismes de plus en plus complexes pour échanger de l'argent qui prenait aussi une forme de plus en plus complexe. Dame Mathématique avait aussi rendu quelques petits services à Dame Politique, mais ils étaient très limités. Dame Mathématique s'y appliqua avec soin mais les contacts entre les deux ne se faisaient guère. Il s'agissait de calculer les superficies de quelques surfaces, d'établir un calendrier fiable. Une fois ce travail fait, Dame Politique laissa tomber Dame Mathématique, car elle trouvait sa conversation rebutante. Le commerce s'organisa et les règles complexes se multipliaient, seule Dame Economie pouvait les comprendre. Alors Dame Economie parlait beaucoup avec Dame Mathématique. Cette dernière entretenait cependant une relation cachée. Dame Economie et Dame Politique le savaient mais ne divulguèrent pas l'horrible secret. Dame Mathématique voyait de temps en temps Monsieur Guerre. En fait Monsieur Guerre devenait de plus en plus lié avec Madame Mathématique. Elle par contre, n'aimait pas cette relation trop violente à son goût ,mais elle n'avait pas trop les moyens de résister aux assauts de Monsieur Guerre. C'était là presque un viol, un secret de famille qui ne devait jamais éclater au grand jour. Et puis les choses se complexifièrent et s'accélérèrent depuis que Madame Mathématique fût en mesure d'accoucher d'un enfant qu'elle appela Informatique. Dame Mathématique s'en occupa fort bien , elle lui appris ses limites et ses possibilités. Elle le fit grandir à l'abri des regards puis le montra à tous. Voyant la beauté de l'adolescent, Dame Economie, Monsieur Guerre et Dame Politique le courtisèrent. Tout semblait sourire à notre adolescent dynamique. Il oeuvrait vite et bien et menait presque toutes les missions qui lui était confiées à leur terme. Il y avait bien parfois quelques faux pas. Informatique appelait ça ses bugs. Maman était au courant et les surveillait de près. Et puis chacun usait et abusait presque d'Informatique sans trop se soucier de ses besoins propres. Même Dame Politique ne s'étonnait pas que la presque totalité de ses décisions et de ses actions reposait sur les épaules d'Informatique. C'était encore pire pour Dame Economie qui en est presque parvenue à croire que les résultats d'Informatique coïncidaient avec la réalité. Dame Politique fit aussi appel à Informatique lorsqu'il fallait prendre une décision concernant la modification du climat de Gaïa. Informatique lui répondit que ce n'était pas de son ressort de prendre des décisions ou d'interpréter ses résultats en termes d'actions. Mais Politique était perdue et puis il fallait agir, alors Informatique se trouva au coeur des décisions de Politique. Cette exposition était difficile pour notre adolescent qui n'en avait pas l'habitude, mais il s'y plia. Bien sûr les armes n'étaient pas égales , Politique avait une habitude certaine de la chose alors qu'Informatique n'était qu'à ses premiers pas dans l'arène. La tempête se calma lorsque Politique eût un discours suffisamment construit pour se passer de la présence d'Informatique. Informatique se reposa un peu lorsque Economie revint frapper à la porte alors qu'il était entrain de faire une partie de jeu vidéo avec ses copains. Elle lui expliqua que ce qu'il avait fait venait de s'écrouler. Informatique avait pris de l'assurance et n'hésita à lui répondre que s'il était comme ça c'est parce que sa mère l'avait fait comme ça, alors si elle voulait en savoir plus elle n'avait qu'à s'adresser à elle. Economie repartit doucement omettant bien de dire qu'elle voyait régulièrement et cela depuis un certain temps, Dame Mathématique. Elles se racontaient toujours un peu toujours la même chose, c'est à dire qu'en "moyenne" les choses se passent à peu près toujours de la même façon. Dame Mathématique essayait bien de lui expliquer que ça ne sera  pas toujours ainsi que ça se passera, mais Dame Economie se satisfaisait bien de la situation. Sauf bien sûr lorsque tout commença à s'emballer. Alors Dame Economie eût peur d'affronter seule la très dure Dame Mathématique et demanda à Dame Politique de l'assister. Pour sauver la face Dame Economie accusa de façon presque frontale Dame Mathématique devant Dame Politique de la responsabilité de la situation actuelle. Dame Politique fit une petite courbette à Dame Mathématique, surprise de la voir d'aussi près pour lui répondre palement qu'elle était enchantée de la connaître. Ce à quoi Dame Mathématique lui répondit de façon brutale, que si elle ne la connaissait pas, la réciproque n'était pas vraie. Informatique lui parla en effet de Politique à tous les repas alors qu'il travaillait sur le réchauffement climatique. Elle dût d'ailleurs mettre la main à la pâte pour l'aider à faire ses devoirs. Dame Mathématique expliqua donc à Dame Politique et Dame Economie que si elles s'appuyaient entièrement sur des résultats d'Informatique et d'elle-même, ils devaient être certains de pouvoir le faire et que ce n'était pas à elle de répondre à cette question.

C'est ainsi, je vous l'affirme, qu'eût lieu la première vraie rencontre de Mathématique avec Politique.

Par contre je ne sais pas ce que fait Monsieur Guerre en ce moment.

Je ne sais pas non plus ce qu'il va advenir des relations entre ces trois Dames, mais c'est certain, dorénavent Dame Politique et Dame Mathématique sont amenées à se rencontrer beaucoup plus souvent.

Je ne sais pas à laquelle des deux, cela fait le plus peur.