"La preuve est à l'œuvre partout, dans toutes les activités théoriques et pratiques, elle est pourtant très difficile à définir tant les formes qu'elle revêt sont diverses.f. Mais si au lieu de partir des théories et formalismes logiques, on s'intéresse à "la caractérisation des activités probatoiresf et si l'on réfléchit alors sur la preuve "comme activité transdisciplinairef (p. 1), ne pourrons-nous un peu mieux comprendre comment nous "prouvons" la légitimité (je n'ose écrire : "la vérité") de nos connaissances, et ce que "valent" nos preuves ?

L'intelligence artificielle propose alors un "point de vue à partir duquel il est possible d'effectuer cet examenf (p. 1). Ce changement de point de vue irritera peut etre les tenants des disciplines qui se prétendent volontiers propriétaires des "vraies méthodes de preuves", que ce soit la logique formelle, la géométrie ou l'arithmétique, mais il va s'avérer manifestement pertinent : En nous devenant plus intelligible, l'activité probatoire, le désir et le plaisir de "prouver" , de se prouver à soi même et de prouver aux autres, vont se révéler à la fois plus sages et plus puissants.

Tel est, je crois, le projet que se sont proposés les contributeurs de ce recueil original et fort bienvenu dans nos cultures contemporaines, dés lors que l'on désacralise les connaissances que l'on enseigne et auxquelles on se réfère pour élaborer nos actions et pour convaincre de leur légitimité. En faisant appel au concours de chercheurs expérimentés en I. A. et en sciences de la cognition, accoutumés à exercer leur savoir dans des champs disciplinaires différents, de l'archéologie à la didactique par le droit ou la géométrie, les deux animateurs de ce dossier nous font bénéficier d'un bel éventail d'arguments révélateurs de la richesse polyphonique de ce concept apparemment simple de "preuve "

L'extréme intérêt de "l'activité probatoiref est de nous inciter à expliciter la démarche modélisatrice impliquée dans le raisonnement probatoire : la preuve est d'abord un exercice de construction: Pour permettre "la pratique de l'échange, dialogue, argumentation" (p. 3), elle passe par un exercice de "transmissionf de "systèmes de symboles ", exercice qui s'est canonisé en de multiples formes. Certes "la pensée mathématique frappe plus que tout autre par sa réglementation des procédures de justification f(p. 4), mais il existe manifestement, en mathématique comme ailleurs "d'autres formes de justification des propositions f. Si bien que l'on doit s'interroger sur les raisons de "cette prédominance de la preuve mathématiquef.

Question qui va servir de fil directeur à cette exploration. Au lieu de prendre le risque de remettre en question la légitimité et la supériorité intrinsèque des formalismes logiques, (ce que le lecteur sera librement tenté de faire pour son compte ), les auteurs vont s'efforcer de décrire et d'interpréter les activités probatoires, et les processus cognitifs computables par lesquels nous pouvons les décrire et ainsi les comprendre. On diagnostique ainsi au sein de l'activité probatoire, quelques fortes et ancestrales tensions : Tensions entre l'idéalisme platonicien et le pragmatisme aristotélicien, (pourrait-on dire aujourd'hui pour faire image au prix de quelques anachronismes), et tensions entre "l'unité de son projet et la diversité de ses manifestationsf, que l'expérience modélisatrice de l'I. A. va permettre d'examiner de façon originale et pertinente.

Pourtant dés le début, j'ai crains que le propos ne s'enferme dans un moule épistémologique fermé, un peu plus grand que le moule académique habituel, mais pourtant vite clôt : la discussion des "implications épistémologiques du cognitivismef, brillamment rédigée par Claude Imbert semble retomber sur le butoir structuraliste habituel. Lorsqu'elle écrit "d'un coté, on posera que toute science est d'abord descriptionf, ma joie est de courte durée, car elle ajoute aussitôt " qu'elle tire sa pertinence et son autorité de sa capacité à faire émerger les structures les plus générales et les plus profondes de ce que nous appelons réalitéf (p. 33). Allons nous retomber dans le travers usuel qui veut que la description (Produite par qui ? Selon quelles règles ? Dans quel contexte ? A quelles fins ? ) donne la structure scientifique (présumée unique) et donc l'explication de la réalité ? C Imbert évoque en conclusion "l'échec de l'épistémologie classiquef par une allusion originale "aux âmes diviséesf du "Monsieur Test" de Valéry. Mais on a envie alors de lui demander alors de relire quelques autres méditations épistémologiques de P.Valéry " Mon système est de représenter et non d'expliquer - Cahiers, 1937, - Je n'ai jamais cru aux explication, .mais j'ai cru qu'il fallait chercher des représentations sur lesquelles on put opérer, comme on travaille sur une carte, ou l'ingénieur sur une épure, etc. , et qui puissent servir à faire - Cahiers 1942 - f. Ce qui bien sur nous conduira à une question plus audacieuse : quelle est l'activité probatoire que nous mettons en œuvre lorsque nous nous exerçons à "computer des symboles ", autrement dit à tâtonner, pour inférer quelques propositions que nous tiendrons pour pertinentes ici et maintenant ? Mais en écartant d'emblée la question du statut épistémologique de la modélisation, ne risque t on pas de s'interdire de pouvoir au moins l'aborder ?

J'appréhendais cette impasse en lisant les lignes expéditives que C Imbert consacre à "l'échec de programme plus ambitieux, tel le "General Problem Solver" des années soixantef (p; 32). Le mot "échec " est manifestement inadéquat pour rendre compte de la contribution de GPS dés 1958 aux premiers programmes d'I. A. de démonstration de théorème (et donc de simulation informatique d'activité probatoire par investigation fins-moyens-fins-… ). Au-delà de cette pique littéraire, c'est l'inattention de C Imbert (et avec elle de presque tous les autres auteurs de ce dossier) aux contributions décisives de H.A Simon et A.Newell à l'étude des processus cognitifs en jeu dans les activités probatoire qui attire mon attention sur les réductions entraînées par cette inutile "fermeture épistémique" du propos. "Human Problem Solving " parut en 1971, et depuis trente ans, la communauté des chercheurs en I. A. s'est, presque à son insu, appropriée l'essentiel de son apport sur la modélisation des processus cognitifs. Mais hélas la légitimation d'une épistémologie de la modélisation par systèmes de symboles computables dont l'œuvre était porteuse (et que H Simon a abondamment exposé et commenté ultérieurement, semble encore ignorée. D'où l'impression que j'ai eue en lisant plusieurs de ces études, de voir en noir et blanc un film dont je pressentais qu'il avait été réalisé en couleur.

Il reste que l'article d'ouverture de C. Imbert a le réel mérite de proposer une discussion épistémologique stimulante de la question initiale : "La connaissance calculée est-elle plus assurée que la connaissance délibérée ?" , et cela introduit fort bien l'ouvrage.

Je ne peux m'arrêter ici avec la même attention à la discussion des autres études d'introduction historique et épistémique qui construisent la première partie de l'ouvrage, mais je souhaite mentionner le vif intérêt que m'a valu l'étude de K. Dosen sur "Le Programme de Hilbert f (. 87 +). J'avais gardé, de ma lecture des remarquables introductions et traductions de J.Largeault : "Intuitionisme et Théorie de la Démonstration" (1992. - cf. ma note de lecture MCX, Cahier des Lectures MCX n° 6, http://archive.mcxapc.org/lectures/?a=display&ID=487 ), le souvenir d'une contradiction diffuse dans la position dramatiquement agressive de Hilbert contre L. J. Brouwer : Formalisme contre Intuitionisme, certes, mais dans les deux écoles, pouvait on échapper à la convention constructiviste ? Pour etre convainquant, un raisonnement ne doit-il pas être artificiellement construit à l'aide de systèmes de symboles eux même artificiellement construits. En bannissant Brouwer, Hilbert pouvait-il légitimement bannir du même coup (pour plus d'un demi-siècle !) le constructivisme épistémologique ? Je trouve dans l'étude de K. Dosen une confirmation de la légitimité de cette interrogation, qui avive ma prudence devant l'assurance épistémologique de bien des mathématiciens : Je cite sa conclusion qui semble, textes à l'appui, bien argumentée: "Le formalisme de Hilbert se trouve quelque part entre le formalisme pur et le constructivisme, tout en étant d'accord avec le platonisme dans l'acceptation des méthodes des mathématiques classiquesf. ( p. 94) Un tel "jugement de Salomonf est il digne d'un des théoriciens les plus illustres des mathématiques de la démonstration ? Il sera désormais permis d'en douter. C'est je crois ce que cherche à souligner J. Sallantin et J;-J. Szczeciniarz dans leur introduction : "Mais la conception de la preuve comme ensemble de dérivations formelles (Hilbert) ne reflète pas la vérité des mathématiques. Elle set plutôt une idéalisation illusoire du rôle de la compréhension en mathématique f (p. 11). Une idéalisation illusoire ! Dire que des millions de citoyens ont appris à l'école que "si cela est mathématiquement prouvé, cela est vrai " ! (On se souvient de cette déclaration fracassante d'un célèbre économiste - mathématicien dans les années quatre vingt: "La supériorité du libéralisme économique est mathématiquement prouvée". Ce qui ne l'a pas empêché d'obtenir un prix Nobel !).

Ajouterai-je un regret ? : une partie de l'argumentation de K.Dosen reprend des développements de l'introduction de J.Largeault qu'il devait connaître lorsqu'il a rédigé son étude. N'aurait-il pas du le mentionner au moins dans sa bibliographie qui, a une exception prés, est exclusivement anglo saxonne ou germanique. Les autres auteurs, historiens de la logique auraient du, il est vrai, lui donner l'exemple. Pour qui souhaite enrichir sa propre intelligence de son "activité probatoire", le détour par les introductions et les traductions de J.Largeault sera, je crois, bienvenu.

Les deux dernières parties de l'ouvrage retiendront sans doute plus l'attention des praticiens car elles sont rédigées par des chercheurs qui s'exercent effectivement à modéliser et à informatiser leur activité probatoire. Chaque lecteur selon ses centres d'intérêt du moment, privilégiera tel ou tel d'entre eux. Je ne peux ici que mentionner succinctement ceux d'entre eux qui ont d'avantage retenu mon attention, à seule fin d'inciter le lecteur à élucider ses propres préférences.

L'article de J.Pitrat est, comme à l'accoutumé, fort stimulant, dés son titre : "Vers un méta mathématicien artificielf. Il s'ouvre sur une proposition que les enseignants en mathématiques n'aiment guère habituellement: "Pratiquement, il est souvent utile d'étudier l'énoncé du problème proposé ; cela permet de changer la formulation du problèmef (p. 117). Ce qui le conduit à s'interroger sur les processus cognitifs et sur les heuristiques que nous mettons en oeuvre pour modifier cette formulation. Il illustre son propos par l'exemple, (emprunté à H. Simon, 1969, page 131 de la 3° édition de 1996), du problème du "tic-tac-toe" qui peut etre transformé en un problème de carré magique de somme 15 ; Puis il l'illustre par la discussion des performances de quelques programmes de "démonstration de théorèmes" (EURISKO, THEOREME, …). Sa conclusion me semble trés légitime, et déborde le champ de "la preuve en I. A." : " je ne pense pas que l'avenir appartienne aux systèmes qui se contentent d'utiliser au maximum la vitesse des ordinateurs en développant des arborescences énormes. Le progrès viendra plutôt de systèmes qui ont encore davantage de capacités de manipuler le problème qu'ils traitent, et d'examiner leur propre comportement f(p. 136. J.Pitrat avait développé cet argument dans "Métaconnaissance, le futur de l'I. A. cf. Note de lecture MCX , Cahier n° 4 : http://archive.mcxapc.org/lectures/?a=display&ID=423 )

L'étude de N.Balatchev, "Apprendre la preuvef, ne surprendra pas les lecteurs qui ont eu la chance de réfléchir sur son introduction et sa traduction française de la thése de I. Lakatos ("Preuves et réfutations. Essai sur la Logique de la découverte mathématiquef, cf. Note de lecture MCX, Cahier N° 20, 1999, http://archive.mcxapc.org/lectures/?a=display&ID=296 .). On comprend mieux, en le lisant pourquoi les éditeurs de ce dossier sur le concept de preuve ont tenté de le centrer sur "l'activité probatoire f plutôt que sur la preuve. En distinguant "preuves pragmatiques et preuves intellectuelles f (p. 200 ), et en discutant soigneusement les processus de preuves ( et d'enseignement de la preuve ) en géométrie, il met fort heureusement en valeur le rôle du "voir" dans le raisonnement probatoire : "la source de la connaissance est dans l'action, et la forme la plus élémentaire d'une preuve est l'ostension : les opérations et les objets qu'elle mobilise sont donnés à voirf. Ce qui le conduit à nous inviter à relire "Preuves et réfutationsf : "Le modèle épistémologique proposé par Lakatos pour analyser les processus de preuve, et au-delà la construction des connaissances mathématiques, ouvre pour la première fois une perspective de solution au problème de l'apprentissage de la démonstrationf (p. 209). Quel dommage que, pas plus que les autres auteurs de ce dossier (sauf une fois, J.Pitrat), N Balatchev ne s'intéresse pas encore aux travaux de H.A. Simon et A. Newell, sur la formulation et la programmation des heuristiques, (H.Simon, "Models of Discovery, 1977f) et sur les raisonnements sur les schémas graphiques ("Why a diagram is (sometimes) worth ten thousand words, 1987f). Les illustrations qu'il propose à partir de programmes de type "Micro monde" tels que Logo ou Cabri-Euclyde, ont entre autres mérites, celui de mettre valeur "l'intelligence ouverte au débat critiquef (p. 233) dans l'apprentissage de la preuve. Mais pour cela souligne t il, "l'I. A. doit s'ouvrir à une socialisation qui peut remettre en question ce qu'elle produit f (p. 234). Proposition qui est pertinente pour toutes les disciplines et pas seulement pour l'I. A. mais celle ci est bien placée pour donner le bon exemple !

L'étude de J.C. Gardin, M. Renaud et MS Lagrange, "Le raisonnement historique à l'épreuve de l'I. A.f fait de "l'épreuve de l'I. A. dans les SHS f (et ici plus spécifiquement l'archéologie), la preuve de la légitimité d'un "relativisme d'excellent aloi…qui ne soit pas réservé aux seules vues de Sirius, philosophiques ou méthodologiques, mais qui… s'affirme aussi dans les travaux de terrain …f (p. 366). Propos non-conformistes, mais fort bien argumentés et illustrés par l'examen de "systèmes experts destinés à l'interprétation de sites proto urbainsf tels que PALAMEDE. Cette brève et originale étude m'a incité à rouvrir les "Essais d'épistémologie pratique en sciences humainef que J.C. Gardin et ses collègues avaient publiés en 1981 et ré édités en 1987 sous un titre pertinent "La Logique du Plausiblef (Editions de la MSH, Paris). J'y ai retrouvé une "prophétief que je crois si pertinente que pour ma part j'en ferai volontiers un projet pour le développement de la recherche scientifique légitimée sinon prouvée dans nos sociétés contemporaines : "Le temps est proche, j'en suis convaincu, où les consommateurs obligés de nos écrits, jusqu'ici respectueux et soumis, demanderont des comptes aux producteurs que nous sommes, sous forme de défis épistémologiques... concernant la raison d'etre de ces écrits …f (p. 296).

N'est ce pas à l'arrivée de ce temps qui verra les citoyens interroger les scientifiques sur la légitimité épistémologiques des connaissances qu'ils produisent, en leur demandant non seulement d'en rendre compte, mais aussi d'en rendre raison : Qu'elles soient au moins plausibles ! N'est-ce ainsi que se légitime "l'épreuve de la preuvef?

Et par là même que se légitime et nous devient importante la stimulante réflexion que nous propose J. Sallantin, J-J. Szczeciniarz et les chercheurs qu'ils ont réunis autours du "concept de preuvef. Les quelques regrets que l'on a mentionnés au fil de la lecture n'enlèvent rien à l' intérêt qu'elle nous vaut. On en demande "encore plus", plus ouvert aussi sur les contributions de J.Dewey (La logique, théorie de l'enquête), de G.Polya (Les mathématiques du raisonnement plausible), de J-B. Grize (Logique Naturelle et communication), et bien sûr, d'A.Newell et H.A. Simon. Mais ne gâchons pas notre plaisir sous prétexte qu'il pourrait etre plus ample.

J.-L. Le Moigne