Je trouve ce commentaire bien plus intéressant que la vidéo de Mr Phi (dont je ne suis pas un grand amateur), mais il y a une réaction encore plus intéressante, à savoir l'article de David Bessis auquel renvoie gro-tsen : the fall of the theorem economy. Article que je conseille de lire pour ceux intéressés par les progrès des LLM en raisonnement et assistant pour la mathématique pure. Je dois avouer que je ne m'attendais pas à des progrès aussi rapide en la matière et que j'aurais plus misés sur la recherche de preuves formalisées en Lean/Rocq/Agda, que via une approche moins formelle en langue naturelle (telle qu'elle est pratiquée par les êtres humains).
Mais au-delà du problème de la distance unitaire, j'ai appris l'existence, via l'article de David Bessis, du projet First proof. Il s'agit d'une expérience menée par des mathématiciens qui mettent au défi les entreprises de LLM (à l'aide d'agents) de résoudre dix problèmes en complète autonomie (sans aide humaine sur le chemin à suivre pour les preuves), puis de les soumettre à une revue par les paires pour avis à publication (comme une revue le ferait pour un chercheur humain). Les problèmes sont choisis parmi des extensions de travaux publiés par les dits chercheurs du projet et correspondent à des théorèmes qu'ils ont prouvé mais non encore publiés. Ils en sont à la deuxième session de leur test :
6 à 8 problèmes furent résolus avec validation pour publication (mais une dead line courte d'une semaine entre l'annonce du projet et les réponses à fournir) ;
la deuxième sessions s'est tenue sur plusieurs mois, et si je compte bien (cf le dépôt github) 7 réponses ont passé la validation par les paires pour publication.
Cela étant, ces progrès indéniables auraient pu mériter un traitement philosophique plus intéressant que ce qu'en fait Mr Phi. Tout d'abord, ce qui semble évident est une question de philosophie des mathématiques et qui renvoie à la question simple de sa propre définition Qu'est-ce que les mathématiques ? C'est en partie un clin d'œil à Laurent Claessens (l'auteur du Frido) qui dans un autre lien demande une définition de l'intelligence. Cette question de la définition est traitée dans un autre article, on ne peut plus intéressant de David Bessis, we had been wrong about mathematics since 2300 years. Le titre est aussi racoleur que celui de la vidéo de Mr Phi, mais le contenu philosophique nettement supérieur. Et ceux qui prétendent que les LLM comprennent ce qu'ils font pour avoir de tels résultats donnent la victoire sans hésitation aux formalistes dans les débats philosophiques sur la nature des mathématiques (position que n'a jamais pu tenir sérieusement aucun mathématicien professionnel, bien au contraire ils sont tous plus ou moins platonistes).
Viens ensuite la question : mais au fond, pourquoi fait-on des mathématiques et à quoi cela sert-il ? Celle-ci je la choisis en référence à la conclusion du premier article de David Bessis et celui-ci de Gro-tsen. On y sent les anciens élèves de la rue d'Ulm et l'influence de Bourbaki. Il cite Jacobi qui fut choisis par Jean Dieudonné pour l'épitaphe et le titre d'un de ses ouvrages de vulgarisation (il est le seul mathématicien que qui fut reçu par Bernard Pivot pour la présentation de son livre, on trouve facilement la vidéo dans les archives de l'INA, elle vaut le coup d'œil).
Il est vrai que M. Fourier avait l'opinion que le but principal des mathématiques était l'utilité publique et l'explication des phénomènes naturels ; mais un philosophe comme lui aurait dû savoir que le but unique de la science, c'est l'honneur de l'esprit humain, et que sous ce titre, une question de nombres vaut autant qu'une question du système du monde.
La plupart des mathématiciens purs se moquent de savoir si leur travaux ont une utilité technico-pratique. Mais alors, comme se questionne David Bessis, pourquoi ces entreprises de la tech investissent-elles de l'argent sur un tel marché de niche pour qui de tels outils n'est pas ardemment désirés ? Quelles idées ont-elles derrière la tête ?
En contrepoint de la citation de Jacobi et en lien avec la philosophie et la notion d'intelligence, je me permet de citer mon maître :
C'est par conséquent une objection aussi mal avisée qu'injuste que les esprits superficiels adressent aux grands hommes qui consacrent aux sciences des soins laborieux lorsqu'ils viennent demander: à quoi cela sert-il ? On ne doit en aucun cas poser une telle question quand l'on prétend s'occuper de science. À supposer qu'une science ne puisse apporter d'explication que sur un quelconque objet possible, de ce seul fait son utilité serait déjà suffisante. Toute connaissance logiquement parfaite a toujours quelque utilité possible : même si elle nous échappe jusqu'à présent, il se peut que la postérité la découvre. Si en cultivant les sciences on n'avait jamais mesuré l'utilité qu'au profit matériel qu'on pourrait en retirer, nous n'aurions pas l'arithmétique ni la géométrie. Aussi bien notre intelligence est ainsi conformée qu'elle trouve satisfaction dans la simple connaissance, et même une satisfaction plus grande que dans l'utilité qui en résulte. Platon l'avait déjà remarqué. L'homme y prend conscience de sa valeur propre; il a la sensation de ce qui se nomme : avoir l'intelligence. Les hommes qui ne sentent pas cela doivent envier les bêtes. La valeur intrinsèque que les connaissances tiennent de leur perfection logique est incomparbale avec leur valeur extrinsèque, qu'elles tirent de leur application.
Kant, Logique.
On pourrait continuer sur la distinction opérée par Socrate entre le philodoxe et le philosohe dans la République de Platon (au livre V, si je me souviens bien), mais par manque de temps je ne développerai pas ce point (peut être dans un autre commentaire).
Enfin pour ceux qui se demanderait pourquoi je glisse encore du Kant dans le débat, c'est tout simple. La perfection logique dans l'exécution de la démonstration est unanimement reconnue par les mathématiciens professionnels comme étant la preuve formalisée dans un logiciel comme Lean, Rocq ou Agda. Au coeur des ces logiciels résident un type checker fondé sur la théorie des types de Pier Martin Lof. Dans un article intitulé analytic and syntehic judgment in type theory, ce dernier rappel deux points. Le premier étant la distinction introduit, par Kant, entre jugement analytique et jugement synthétique ainsi que sa thèse centrale qui est que tous les jugements mathématiques sont synthétiques a priori. C'est cette thèse qui fut combattu à la fin du dix neuvième par les logicistes, qui foutu le bordel dans les fondements des mathématiques, mais chemin faisant on a eu les travaux de Gödel et Turing. Le second étant qu'en fin d'article il écrit :
So you have this formulation, which I have already quoted twice, mathematical knowledge through the construction of concepts, a splendid formulation which no doubt had a fruitful influence on Brouwer, and to my mind it is justifiable to say that intuitionism is a developpemnt of an essential Kantian position in the foundation of mathematics.
La formulation est là et répond à la première question philosophique que je posais : qu'est-ce que les mathématiques ? À cela Kant répondais : c'est la connaissance rationnelle par la construction de concepts, pour la distinguer de la philosophie qui est la connaissance rationnelle par concepts. Ce qui répond au passage à la question de David Bessis dans son article sur la définition des mathématiques : les intuitionnistes ont une définition très claire de ce que sont les mathématiques, ils ne sont ni platonistes, ni formalistes, mais pour une raison que j'ignore il semble ignorer cette position.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
L'intelligence de l'intelligence
L'artificielle intelligence de l'intelligence
L'intelligence de l'intelligence artificielle
L'artificielle intelligence de l'intelligence artificielle
Voire des trucs moins binaires
j'y verrais (ou pas) plus clair
"Si tous les cons volaient, il ferait nuit" F. Dard
Oui c'est scandaleux que les LLM n'ait pas répondu ! D'autant que les problèmes NP complet sont parfaitement décidables, juste long à calculer, mais ce sont des théorèmes dont la démonstration ou refutation est parfaitement automatisable. D'ailleurs ma machine le fait à chaque fois que j'installe un paquet OCaml via le gestionnaire de paquets opam (il doit résoudre un problème NP complet).
Voilà un titre choc : des millions de personnes par jour font démontrer automatiquement des théorèmes par leur ordinateur à chaque qu'il font apt install et personne n'en parle !
Si on demande à gemini un apt install firefox, il hallucine à tous les coups et installe chrome. :-P
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Une pas intelligence humaine dirait si P=0 ou N=1 mais on va me dire que je suis hors sujet. Algorithmiquement P=NP n'est que le calcul du terme suivant d'une suite géométrique. Encore hors sujet. Et informatiquement on cherche plutôt P==NP. Certes toujours hors sujet. Pas prêt pour les problèmes weirdos.
Je ne le suis pas plus, mais il ne faut pas pour autant être impressioné par ce qu'il s'est passé.
Avec sa remarque, BAud m'a donné le moyen d'expliquer simplement ce qui a eu lieu, et si cela peut sembler impressionnant, il faut relativiser.
La preuve automatique de théorèmes par un ordinateur cela n'a rien de nouveau, et c'est le quotidien de tous les utilisateurs d'une distribution Linux.
Tu veux installer firefox, tu conjectures que tu le peux, il y a deux cas :
l'installation marche, ta conjecture s'est avérée exacte ;
l'installation échoue, il y a des conflits, tu es réfutée.
Dans le cas de problème de la distance unitaire, on s'est retrouvée dans le second cas, voilà ce qui s'est passé. Le LLM a construit un contre-exemple, tout comme ton gestionnaire (apt ou un autre) a trouvé des conflits : les conflits qu'il explicite sont ses contre-exemples.
Dans le cas des gestionnaires de paquets, on se retrouve dans du NP-complet, c'est compliqué mais parfaitement décidable.
Dans le cas mathématique général, le procédé de recherche de preuves ou de réfutations est indécidable : c'est ce qu'ont montré Gödel et Turing. Comme le dit Martin-Löf dans sa conférence, pour parler le langage de Kant, avec un problème SAT (NP complet, le cas des gestionnaires de paquets) on est dans de l'analytique, tandis que le cas général des énoncés mathématique (dont la conjecture d'Erdös) est celui du synthétique a priori qui est indécidable. Il faut alors trouver d'autres méthodes pour y arriver, et c'est là qu'entre en jeu les méthodes formelles.
Pour l'industrie, on trouve par exemple :
- alt-ergo par l'équipe qui développe aussi opam le gestionnaire de paquets pour OCaml ;
- why3 qui est semi-automatique, certaines sont renvoyées vers Rocq pour un traitement manuel ;
- la méthode B qui fait fonctionner les métros automatiques de Paris.
Ce n'est pas un domaine inexploré de l'informatique, loin de là, ce sont mêmes ces questions, issues des mathématiques pures, qui font que nous avons aujourd'hui des ordinateurs. Mais personne au monde n'est venu affirmé que les machines étaient intelligentes grâce à cela et c'est incommensurablement plus fiable que n'importe quel perroquet stochastique. Gerard Berry qui a occupé la chaire au Collège de France avant Xavier Leroy, qui a fait toute sa carrière dans ce domaine de recherche, n'a jamais cessé de répéter qu'un ordinateur étant complément con : il calcule a une vitesse qui écrase tout être humain, mais il est con comme un balai.
Si l'on prend la méthode B, on peut faire ce titre racoleur : des millions de personnes de part de le monde voyage dans de métros automatiques grâce a des conjectures prouvées ou réfutées automatiquement (ou semi-automatiquement) par un ordinateur… sauf le Collège de France. ;-)
Jean-Raymond Abrial, l'inventeur de la méthode, a donné une conférence sur le sujet au Collège de France, invité par Gérard Berry. Je ne l'ai pas trouvé avec une rapide recherche, mais je suis sûr qu'elle existe, si quelqu'un est motivé.
Pour faire fonctionner la ligne 14 à Paris, les ingénieurs qui l'on conçu ont fait comme Erdös : de la formalisation et de la conjecture, et la machine se charge de confirmer ou d'infirmer leur intuition.
Néanmoins, dans le cas du métro automatique (comme pour un gestionnaires de paquets), on n'est pas intéressé par le contenu de la preuve elle-même. Si cela produit un gloubi boulga, on s'en fout, on veut juste la réponse mais avec la certitude que la machine ne se trompe pas (donc exit les perroquets). Par contre si l'on cherche une preuve formelle, que son contenu est ce qui nous importe le plus (cas des mathématiques pures ou même de la programmation usuelle, c'est la même chose par Curry-Howard), on envoie à la poubelle le code AI slop parce que son API est tout a chier et sans intérêt. D'où la réaction de Patrick Massot :
I think the situation is pretty clear: AI companies, and especially Math Inc, will indeed thoroughly bomb this area to turn it into a giant radioactive wasteland that will never be able to sustain life again, so we will never get the benefits expected from formalization (improved understanding and accessibility). I strongly advise young people to contribute to less shiny projects that are less likely to be destroyed.
Et je rajoute : quel est donc le projet politique de ces entreprises de la big tech pour vouloir jouer à ce jeu là ?
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
ou de me rappeler à chaque fois le souvenir douloureux de l'étude de "la critique de la raison pure" pendant mon année de Terminale il y a très longtemps. Un cauchemar.
"Si tous les cons volaient, il ferait nuit" F. Dard
C'est parce que d'une part la philosophie en terminale est une particularité française et que d'autre part c'est incomprhénsible pour une élève de terminale. Si tu lis l'article de Martin-Lof, il explique par exemple que sa déduction des catégories est identique dans le principe à ce que les mathématiciens appellent la correspondance de Curry-Howard.
Les mathématiciens sont plus raisonnables dans la formation de la jeunesse. Personnellement, ce résultat mathématique m'a été enseigné quand j'étais en DEA (Bac +5) : je me suis dit cool, c'est comme Kant mais en plus simple. J'avais justement choisi un DEA en logique mathématique et fondement de l'informatique pour approfondir ma connaissance de la logique et mieux comprendre certains point de la Critique qui me restait obscur.
C'est comme si on disait à un élève de terminale en cours de maths : aujourd'hui on va étudier le théorème d'incomplétude de Gödel et le problème de l'arrêt de Turing, ainsi que leur incidence sur le fondement des mathématiques. Tu penses que ça se passerait bien ?
Ajoute à cela, que les enseignants de philosophie de terminale ne comprennent pas l'ouvrage eux même (Mr Phi en est le parfait exemple) et tu as le parfait cocktail pour du grand n'importe quoi.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Quel genre d’enseignement de la philosophie te paraîtrait meilleur ? Pas de philosophie du tout dans l’enseignement secondaire ? Au contraire, un enseignement beaucoup plus progressif étalé sur plusieurs années de lycée voire de collège ou d’école primaire ? Un enseignement moins centré sur la découverte de textes classiques et davantage sur la réflexion logique ou la découverte spontanée de questions philosophiques ? …
Perso mon expérience (terminale S en 2000-2001) : je croyais qu'on allait « penser ensemble » et que ça serait chouette. En fait non on a bachoté autour de raisonnements, souvent fallacieux, sans même chercher à les déconstruire, avec un prof qui avait lui même du mal à s'y impliquer de façon convaincante. (« Bonjour monsieur, j'ai toujours pas compris pourquoi un pot de fleurs posé sur une table dans un rêve évoque à Freud une connotation sexuelle ? » Depuis j'ai compris sans nul doute que le soucis était chez l'auteur…)
J'ai eu la même expérience mais un peu plus tôt (96-97) et j'ai eu 5 au bac. :-P
Je me méfie toujours des philosophes, il y a de l'excellent comme du pur AI slop dans cette discipline. Je suis né mathématicien, j'ai vécu en mathématicien et je mourrai en mathématicien. Je suis kantien car, de tous les philosophes que j'ai lu, c'est le seul dont j'ai pu dire « nul ne peut entrer ici, s'il n'est géomètre ». ;-)
Peut-être ce passage de la préface de la deuxième édition te semblera moins chiante à lire :
Si donc il n’est pas impossible de léguer à la postérité une métaphysique systématique construite sur le plan de la critique de la raison pure, ce n’est pas un don médiocre à lui faire ; soit que l’on songe simplement à la culture que la raison peut recevoir en général en entrant dans les voies certaines de la science, au lieu d’errer dans le vide et de se livrer à de vaines divagations, comme elle le fait en l’absence de la critique ; soit que l’on cherche un meilleur emploi du temps pour une jeunesse avide de savoir, que le dogmatisme ordinaire encourage de si bonne heure et si fortement à raisonner à perte de vue sur des choses où elle n’entend rien et où elle n’entendra jamais rien, non plus que personne au monde, ou à négliger l’étude des sciences solides pour courir à la recherche de pensées et d’opinions nouvelles.
Kant, Critique de la raison pure
Et pour avoir lu toute son œuvre, ce qu'il entendait par sciences solides, c'était la logique, les mathématiques, la physique… et la métaphysique qu'il s'est efforcé de fonder. ;-)
Après, mon parcours, c'est classe prépa MPSI-MP, licences de mathématique fondamentale, maîtrise de mathématique pure et DEA de logique. C'est en licence que j'ai découvert la Critique pour les mêmes raisons que David Bessis : comprendre la nature de cette science qui occupe mon esprit en permanence, et ce fût une révélation. C'est uniquement depuis ce temps que je m'intéresse à la philosophie. En DEA, il y avait des étudiants issus soit d'un cursus mathématique (comme moi), soit d'un cursus philosophique (ils galéraient un peu sur certains sujets mathématiques, mais nos discussions étaient des plus rafraîchissante).
Cela étant son œuvre ne se limite pas à ce que l'on appelle de nos jours les sciences « dures », il a eu une influence non négligeable sur l'existence d'institutions comme la Sociétés des Nations, l'Organisation des Nations Unies ou encore l'Union Européenne (voir son opuscule Vers la paix perpétuelle). Il a appliqué le même principe que Curry-Howard au domaine du droit et, dans les facultés de droit ou de sciences politiques, il est étudié pour cela. À la question : pourquoi faut-il trois pouvoirs (le législatif, l'exécutif et le judiciaire) ? il répond que c'est nécessaire conformément à la structure formelle d'un syllogisme :
Tous les hommes sont mortels (majeure)
Socrate est un homme (mineure)
donc Socrate est mortel (conclusion)
à la majeure correspond la Loi (le pouvoir législatif), à la mineure correspond le cas ou question de fait dans un procès (le pouvoir exécutif représenté par le procureur) et enfin le juge (pouvoir judiciaire) subsume la mineure sous la majeure pour tirer la conclusion ou sentence.
Et ce qui est drôle, c'est que si l'on regarde un code informatique qui gère des permissions (via Curry-Howard), il suit le même schéma : c'est un tel syllogisme. ;-)
À la question : pourquoi tous les hommes naissent-ils libre et égaux en droit ? Il répond que c'est l'équivalent juridique du principe d'action-réaction chez Newton, et que ces deux principes ont pour fondement la forme logique des jugements disjonctifs (A ou B).
Et là on sort totalement du cadre légitime du recours à la méthode axiomatique (limitée aux mathématiques), mais la structure formelle reste identique : voilà, pour moi, l'essence de ce que Kant a apporté à la philosophie. ;-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Comme le montre mon commentaire en réponse à Polux, je n'ai rien à préconisé pour l'enseignement de la philosophie. Je suis avant tout mathématicien et la philosophie fut pour moi nécessaire pour répondre à mes problèmes. Je laisse aux philosophes des académies le soin d'orchestrer leur enseignement comme ils l'entendent. ;-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Le contenu de l’enseignement de la philosophie ne dépend pas seulement de ce que veulent les philosophes et les professeurs de philosophie, mais aussi de l’importance que la société confère à cet enseignement.
La valeur qu’attribue notre société aux mathématiques est telle que treize ans d’enseignement minimum lui sont consacrés (de l’âge de 3 ans à celui de 16 ans), contre seulement un an pour la philosophie (et ce seulement pour les jeunes qui passent un bac général, soit environ 45 % d’une génération).
13 ans d’étude minimum (et jusque 20 ans d’étude dans le cas de l’obtention de certains masters scientifiques), ça laisse un peu de temps pour organiser un enseignement « raisonnable ».
Pour revenir à la découverte de la pensée de Kant en classe de terminale : je me dis que les professeurs de philosophie sont dans une situation assez difficile. D’un côté : comment réussir à faire découvrir correctement la complexité de la pensée de Kant pendant cette seule année d’enseignement de la philosophie ? D’un autre côté : est-il possible de ne pas aborder ce classique des classiques pendant ce cours de philosophie qui sera probablement le seul de la vie de ces jeunes ?
Je sais bien les contraintes auxquelles ils doivent faire face, ce que je voulais dire dans mon précèdent message est que je ne me sens pas légitime pour leur donner le moindre conseil.
Une idée qui me vient à l'esprit, et qui pourrait profiter au philosophe, est une proposition faîte par Gérard Huet dans un conférence intitulée Fondements de l'informatique, à la croisée des mathématiques, de la logique et de la linguistique (le document est un docx mais il s'ouvre bien avec libre office). Il illustre par deux exemple comment on pourrait faire mettre en pratique ce qui se cache dans Curry-Howard (et donc la logique transcendentale de Kant) sans nécessairement aborder la théorie elle-même (au fond ce qu'expose ces théories est la structure logique de notre esprit, mais cette structure on l'utilise naturellement sans même savoir l'exposer théoriquement).
Les exemples se trouvent à la fin de sa conférence (dans ma version que j'ai convertie en pdf, c'est à la page 20) est commence au paragraphe :
On nous dit « il faut inculquer aux jeunes l’esprit scientifique ». Très bien, mais qu’est ce que ça veut dire au juste, au-delà d’une incantation un peu creuse ?
Le premier exemple consiste à calculer le coût financier du cycle de lavage d'une machine à laver, puis à réfléchir sur le raisonnement qui conduit à la réponse. Si Luc Skywalker me lit, c'est analogue à la discussion que tu as eu avec gUI sur la rentabilité de récupérer l'énergie potentiel sur un vélo électrique : vous avez utilisé la Critique de la raison pure sans le savoir (catégorie de la causalité dans la logique transcendentale). ;-)
Le second consiste à faire de l'analyse grammaticale sur les verbes transitifs et intransitifs, avec pour exemple « le chat mange la souris ».
Puis de montrer que, d'un certain point de vue, les deux situations sont identiques dans notre manière de raisonner.
Pour répondre à cette question :
D’un autre côté : est-il possible de ne pas aborder ce classique des classiques pendant ce cours de philosophie qui sera probablement le seul de la vie de ces jeunes ?
Je dirais absolument oui, il l'a dit lui-même !
Sans entrer dans le détail de son œuvre, je vais juste illustrer pourquoi je dis de lui « nul ne peut entre ici s'il n'est géomètre ». Les géomètres, ou plus généralement les mathématiciens, utilisent pour résoudre leur problème une méthode qu'ils nomment le raisonnement par analyse-synthèse. Pappus d'Alexandrie le décrivait en ces termes :
Analysis, then, takes that which is sought as if it were admitted and passes from it through its successive consequences to something which is admitted as the result of synthesis: for in analysis we admit that which is sought as if it were already done and we inquire what it is from which this results, and again what is the antecedent cause of the latter, and so on, until by so retracing our steps we come upon something already known or belonging to the class of first principles, and such a method we call analysis as being solution backwards.
But in synthesis, reversing the process, we take as already done that which was last arrived at in the analysis and, by arranging in their natural order as consequences what before were antecedents, and successively connecting them one with another, we arrive finally at the construction of what was sought; and this we call synthesis.
Dans l'analyse on va de la conclusion aux prémisses, tandis que dans la synthèse on redescend des prémisses à la conclusion. D'ailleurs, le logiciel d'aide à la preuve Rocq fonctionne ainsi : on prouve la proposition par voie d'analyse, puis, quand on a fini, on écrit qed (quod erat demonstrandum ou cqfd) et le moteur de Rocq effectue la synthèse pour nous.
Je me suis permis cette petite digression parce que certains ouvrages de Kant vont par paire : dans l'un il suit la voie analytique, dans l'autre la voie synthétique. Dans le cas de la Critique de la raison pure, c'est la voie synthétique qui est suivie. Son ouvrage jumeau, qui suit la voie analytique, se nomme les prolégomènes à toute métaphysique future. Ce dernier s'ouvre sur cette avertissement (première phrase de la préface) :
Ces prolégomènes ne sont pas à l’usage des élèves ; ils s’adressent aux maîtres futurs, auxquels même ils doivent servir, non pas pour l’exposition méthodique d’une science toute faite, mais uniquement pour l’invention de cette science.
Ils servent à exposer la voie de découverte (la méthode analytique est la voie de la recherche qui trouve) qui mène à la Critique (dont l'exposé est synthétique).
Partant de là, je doute fort, tout de même, qu'il soit approprier d'aborder cet ouvrage avec des élèves de terminal sans finir dans du n'importe quoi, d'autant que, je le répète, un professeur de terminal ne le comprend peut être pas lui-même.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Après reflexion, j'ai oublié un point. Si les professeurs de philosophie sont sans doute tenter d'aborder l'ouvrage c'est à cause de la notion de liberté, qu'il leur faut traiter dans leur programme.
Si le synthétique a priori mène à des questions sans réponses en mathématique, les propositions indécidables de Gödel et Turing, il en est de même pour le synthétique a priori en philosophie. Chez Kant cela se nomme les antinomies de la raison pure et, comme pour les mathématiques, cela se produit lorsque l'on introduit la récursivité. La plus célèbre de ces antinomies étant la troisième, connue sous sa forme populaire du problème de l'œuf et de la poule, et la réponse de Kant à la question de savoir qui vient en premier est de dire : ni l'un, ni l'autre mais l'homme est libre. :-D
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
Disons que potasser Kant tout au long de l'année alors que tu n'y comprends pas grand chose, c'était pas cool.
Le reste du cours de Philo était plutôt intéressant par contre. Au Bac, j'ai pris le sujet de dissertation sur la Liberté et j'ai eu 15 je crois.
Donc, ça c'est bien passé quand même ;)
"Si tous les cons volaient, il ferait nuit" F. Dard
Les mathématiques donnent le plus éclatant exemple d’une heureuse extension de la raison pure par elle-même et sans le secours de l’expérience. Les exemples sont contagieux, surtout pour cette faculté, qui se flatte naturellement d’avoir toujours le même bonheur qu’elle a eu dans un cas particulier. Aussi la raison pure espère-t-elle pouvoir s’étendre, dans son usage transcendental, avec autant de bonheur et de solidité qu’elle l’a fait dans son usage mathématique, surtout en appliquant ici cette même méthode qui lui a été là d’une si évidente utilité. Il nous importe donc beaucoup de savoir si la méthode qui conduit à la certitude apodictique, et que dans cette dernière science on appelle mathématique, est identique à celle qui sert à chercher cette même certitude dans la philosophie et qui y devrait être appelée dogmatique.
La connaissance philosophique est la connaissance rationnelle par concepts, et la connaissance mathématique la connaissance rationnelle par construction des concepts. Construire un concept, c’est représenter à priori l’intuition qui lui correspond. La construction d’un concept exige donc une intuition non empirique, qui par conséquent, comme intuition, soit un objet singulier, mais qui n’en exprime pas moins, comme construction d’un concept (d’une représentation générale), quelque chose d’universel qui s’applique à toutes les intuitions possibles appartenant au même concept. Ainsi je construis un triangle en représentant l’objet correspondant à ce concept soit par la simple imagination dans l’intuition pure, soit même, d’après celle-ci, sur le papier dans l’intuition empirique, mais dans les deux cas tout à fait à priori, sans en avoir tiré le modèle de quelque expérience. La figure particulière ici décrite est empirique, et pourtant elle sert à exprimer le concept sans nuire à son universalité, parce que, dans cette intuition empirique, on ne songe jamais qu’à l’acte de la construction du concept, auquel beaucoup de déterminations sont tout à fait indifférentes, comme celles de la grandeur, des côtés et des angles, et que l’on fait abstraction de ces différences qui ne changent pas le concept du triangle.
Kant, Critique de la raison pure
Il faut lire la suite aussi, où il explique qu'au sens propre du terme seule la mathématique possède des définitions, raisons pour laquelle les BA des LLM ne savent même pas ce qu'ils demandent lorsqu'ils exigent une définition de l'intelligence. Mais bon, ce sont des adeptes de la métaphysique de bistro. ;-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
# Mise au propre
Posté par Ploufplouf . Évalué à 10 (+10/-0).
La même chose mis en page et plus lisible sur son blog :
http://www.madore.org/~david/weblog/d.2026-06-11.2855.ai-and-math-2.html#d.2026-06-11.2855
[^] # Re: Mise au propre
Posté par Ysabeau 🧶 (courriel, site web personnel, Mastodon) . Évalué à 3 (+0/-0).
Nettement plus lisible, merci.
Je n’ai aucun avis sur systemd
# Au-delà du problème de Erdös
Posté par kantien . Évalué à 4 (+2/-0).
Je trouve ce commentaire bien plus intéressant que la vidéo de Mr Phi (dont je ne suis pas un grand amateur), mais il y a une réaction encore plus intéressante, à savoir l'article de David Bessis auquel renvoie gro-tsen : the fall of the theorem economy. Article que je conseille de lire pour ceux intéressés par les progrès des LLM en raisonnement et assistant pour la mathématique pure. Je dois avouer que je ne m'attendais pas à des progrès aussi rapide en la matière et que j'aurais plus misés sur la recherche de preuves formalisées en Lean/Rocq/Agda, que via une approche moins formelle en langue naturelle (telle qu'elle est pratiquée par les êtres humains).
Mais au-delà du problème de la distance unitaire, j'ai appris l'existence, via l'article de David Bessis, du projet First proof. Il s'agit d'une expérience menée par des mathématiciens qui mettent au défi les entreprises de LLM (à l'aide d'agents) de résoudre dix problèmes en complète autonomie (sans aide humaine sur le chemin à suivre pour les preuves), puis de les soumettre à une revue par les paires pour avis à publication (comme une revue le ferait pour un chercheur humain). Les problèmes sont choisis parmi des extensions de travaux publiés par les dits chercheurs du projet et correspondent à des théorèmes qu'ils ont prouvé mais non encore publiés. Ils en sont à la deuxième session de leur test :
Cela étant, ces progrès indéniables auraient pu mériter un traitement philosophique plus intéressant que ce qu'en fait Mr Phi. Tout d'abord, ce qui semble évident est une question de philosophie des mathématiques et qui renvoie à la question simple de sa propre définition Qu'est-ce que les mathématiques ? C'est en partie un clin d'œil à Laurent Claessens (l'auteur du Frido) qui dans un autre lien demande une définition de l'intelligence. Cette question de la définition est traitée dans un autre article, on ne peut plus intéressant de David Bessis, we had been wrong about mathematics since 2300 years. Le titre est aussi racoleur que celui de la vidéo de Mr Phi, mais le contenu philosophique nettement supérieur. Et ceux qui prétendent que les LLM comprennent ce qu'ils font pour avoir de tels résultats donnent la victoire sans hésitation aux formalistes dans les débats philosophiques sur la nature des mathématiques (position que n'a jamais pu tenir sérieusement aucun mathématicien professionnel, bien au contraire ils sont tous plus ou moins platonistes).
Viens ensuite la question : mais au fond, pourquoi fait-on des mathématiques et à quoi cela sert-il ? Celle-ci je la choisis en référence à la conclusion du premier article de David Bessis et celui-ci de Gro-tsen. On y sent les anciens élèves de la rue d'Ulm et l'influence de Bourbaki. Il cite Jacobi qui fut choisis par Jean Dieudonné pour l'épitaphe et le titre d'un de ses ouvrages de vulgarisation (il est le seul mathématicien que qui fut reçu par Bernard Pivot pour la présentation de son livre, on trouve facilement la vidéo dans les archives de l'INA, elle vaut le coup d'œil).
La plupart des mathématiciens purs se moquent de savoir si leur travaux ont une utilité technico-pratique. Mais alors, comme se questionne David Bessis, pourquoi ces entreprises de la tech investissent-elles de l'argent sur un tel marché de niche pour qui de tels outils n'est pas ardemment désirés ? Quelles idées ont-elles derrière la tête ?
En contrepoint de la citation de Jacobi et en lien avec la philosophie et la notion d'intelligence, je me permet de citer mon maître :
On pourrait continuer sur la distinction opérée par Socrate entre le philodoxe et le philosohe dans la République de Platon (au livre V, si je me souviens bien), mais par manque de temps je ne développerai pas ce point (peut être dans un autre commentaire).
Enfin pour ceux qui se demanderait pourquoi je glisse encore du Kant dans le débat, c'est tout simple. La perfection logique dans l'exécution de la démonstration est unanimement reconnue par les mathématiciens professionnels comme étant la preuve formalisée dans un logiciel comme Lean, Rocq ou Agda. Au coeur des ces logiciels résident un type checker fondé sur la théorie des types de Pier Martin Lof. Dans un article intitulé analytic and syntehic judgment in type theory, ce dernier rappel deux points. Le premier étant la distinction introduit, par Kant, entre jugement analytique et jugement synthétique ainsi que sa thèse centrale qui est que tous les jugements mathématiques sont synthétiques a priori. C'est cette thèse qui fut combattu à la fin du dix neuvième par les logicistes, qui foutu le bordel dans les fondements des mathématiques, mais chemin faisant on a eu les travaux de Gödel et Turing. Le second étant qu'en fin d'article il écrit :
La formulation est là et répond à la première question philosophique que je posais : qu'est-ce que les mathématiques ? À cela Kant répondais : c'est la connaissance rationnelle par la construction de concepts, pour la distinguer de la philosophie qui est la connaissance rationnelle par concepts. Ce qui répond au passage à la question de David Bessis dans son article sur la définition des mathématiques : les intuitionnistes ont une définition très claire de ce que sont les mathématiques, ils ne sont ni platonistes, ni formalistes, mais pour une raison que j'ignore il semble ignorer cette position.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Au-delà du problème de Erdös
Posté par Luc-Skywalker . Évalué à 2 (+0/-0).
Ça existe ?:
L'intelligence de l'intelligence
L'artificielle intelligence de l'intelligence
L'intelligence de l'intelligence artificielle
L'artificielle intelligence de l'intelligence artificielle
Voire des trucs moins binaires
j'y verrais (ou pas) plus clair
"Si tous les cons volaient, il ferait nuit" F. Dard
[^] # Re: Au-delà du problème de Erdös
Posté par BAud (site web personnel) . Évalué à 3 (+1/-0).
il reste à prouver que
pour certains des cas ;-)
[^] # Re: Au-delà du problème de Erdös
Posté par kantien . Évalué à 3 (+1/-0).
Oui c'est scandaleux que les LLM n'ait pas répondu ! D'autant que les problèmes NP complet sont parfaitement décidables, juste long à calculer, mais ce sont des théorèmes dont la démonstration ou refutation est parfaitement automatisable. D'ailleurs ma machine le fait à chaque fois que j'installe un paquet OCaml via le gestionnaire de paquets
opam(il doit résoudre un problème NP complet).Voilà un titre choc : des millions de personnes par jour font démontrer automatiquement des théorèmes par leur ordinateur à chaque qu'il font
apt installet personne n'en parle !Si on demande à gemini un
apt install firefox, il hallucine à tous les coups et installe chrome. :-PSapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Au-delà du problème de Erdös
Posté par Benoît Sibaud (site web personnel) . Évalué à 3 (+0/-0).
Une pas intelligence humaine dirait si P=0 ou N=1 mais on va me dire que je suis hors sujet. Algorithmiquement P=NP n'est que le calcul du terme suivant d'une suite géométrique. Encore hors sujet. Et informatiquement on cherche plutôt P==NP. Certes toujours hors sujet. Pas prêt pour les problèmes weirdos.
[^] # Re: Au-delà du problème de Erdös
Posté par kantien . Évalué à 2 (+0/-0).
Je ne le suis pas plus, mais il ne faut pas pour autant être impressioné par ce qu'il s'est passé.
Avec sa remarque, BAud m'a donné le moyen d'expliquer simplement ce qui a eu lieu, et si cela peut sembler impressionnant, il faut relativiser.
La preuve automatique de théorèmes par un ordinateur cela n'a rien de nouveau, et c'est le quotidien de tous les utilisateurs d'une distribution Linux.
Tu veux installer
firefox, tu conjectures que tu le peux, il y a deux cas :Dans le cas de problème de la distance unitaire, on s'est retrouvée dans le second cas, voilà ce qui s'est passé. Le LLM a construit un contre-exemple, tout comme ton gestionnaire (
aptou un autre) a trouvé des conflits : les conflits qu'il explicite sont ses contre-exemples.Dans le cas des gestionnaires de paquets, on se retrouve dans du NP-complet, c'est compliqué mais parfaitement décidable.
Dans le cas mathématique général, le procédé de recherche de preuves ou de réfutations est indécidable : c'est ce qu'ont montré Gödel et Turing. Comme le dit Martin-Löf dans sa conférence, pour parler le langage de Kant, avec un problème SAT (NP complet, le cas des gestionnaires de paquets) on est dans de l'analytique, tandis que le cas général des énoncés mathématique (dont la conjecture d'Erdös) est celui du synthétique a priori qui est indécidable. Il faut alors trouver d'autres méthodes pour y arriver, et c'est là qu'entre en jeu les méthodes formelles.
Pour l'industrie, on trouve par exemple :
- alt-ergo par l'équipe qui développe aussi opam le gestionnaire de paquets pour OCaml ;
- why3 qui est semi-automatique, certaines sont renvoyées vers Rocq pour un traitement manuel ;
- la méthode B qui fait fonctionner les métros automatiques de Paris.
Ce n'est pas un domaine inexploré de l'informatique, loin de là, ce sont mêmes ces questions, issues des mathématiques pures, qui font que nous avons aujourd'hui des ordinateurs. Mais personne au monde n'est venu affirmé que les machines étaient intelligentes grâce à cela et c'est incommensurablement plus fiable que n'importe quel perroquet stochastique. Gerard Berry qui a occupé la chaire au Collège de France avant Xavier Leroy, qui a fait toute sa carrière dans ce domaine de recherche, n'a jamais cessé de répéter qu'un ordinateur étant complément con : il calcule a une vitesse qui écrase tout être humain, mais il est con comme un balai.
Si l'on prend la méthode B, on peut faire ce titre racoleur : des millions de personnes de part de le monde voyage dans de métros automatiques grâce a des conjectures prouvées ou réfutées automatiquement (ou semi-automatiquement) par un ordinateur… sauf le Collège de France. ;-)
Jean-Raymond Abrial, l'inventeur de la méthode, a donné une conférence sur le sujet au Collège de France, invité par Gérard Berry. Je ne l'ai pas trouvé avec une rapide recherche, mais je suis sûr qu'elle existe, si quelqu'un est motivé.
Pour faire fonctionner la ligne 14 à Paris, les ingénieurs qui l'on conçu ont fait comme Erdös : de la formalisation et de la conjecture, et la machine se charge de confirmer ou d'infirmer leur intuition.
Néanmoins, dans le cas du métro automatique (comme pour un gestionnaires de paquets), on n'est pas intéressé par le contenu de la preuve elle-même. Si cela produit un gloubi boulga, on s'en fout, on veut juste la réponse mais avec la certitude que la machine ne se trompe pas (donc exit les perroquets). Par contre si l'on cherche une preuve formelle, que son contenu est ce qui nous importe le plus (cas des mathématiques pures ou même de la programmation usuelle, c'est la même chose par Curry-Howard), on envoie à la poubelle le code AI slop parce que son API est tout a chier et sans intérêt. D'où la réaction de Patrick Massot :
Et je rajoute : quel est donc le projet politique de ces entreprises de la big tech pour vouloir jouer à ce jeu là ?
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Au-delà du problème de Erdös
Posté par Pol' uX (site web personnel) . Évalué à 3 (+1/-0).
https://www.college-de-france.fr/fr/agenda/seminaire/prouver-les-programmes-pourquoi-quand-comment/specification-construction-et-verification-de-programmes-le-parcours-une-pensee-scientifique-sur-une
Adhérer à l'April, ça vous tente ?
[^] # Re: Au-delà du problème de Erdös
Posté par kantien . Évalué à 2 (+0/-0).
Merci :D
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Au-delà du problème de Erdös
Posté par serol (site web personnel) . Évalué à 4 (+3/-0).
Perso je reste persuadé que tu t’es donné une contrainte d’écriture à l'Oulipo : réussir à parler de Kant dans tous tes commentaires sur Linuxfr ;)
[^] # Re: Au-delà du problème de Erdös
Posté par Luc-Skywalker . Évalué à 2 (+0/-0).
ou de me rappeler à chaque fois le souvenir douloureux de l'étude de "la critique de la raison pure" pendant mon année de Terminale il y a très longtemps. Un cauchemar.
"Si tous les cons volaient, il ferait nuit" F. Dard
[^] # Re: Au-delà du problème de Erdös
Posté par Benoît Sibaud (site web personnel) . Évalué à 5 (+2/-0).
Kant te re-verrais-je, pays merveilleux…
[^] # Re: Au-delà du problème de Erdös
Posté par Luc-Skywalker . Évalué à 2 (+0/-0).
Ah bien vu :)
C'était en effet à cette époque là
"Si tous les cons volaient, il ferait nuit" F. Dard
[^] # Re: Au-delà du problème de Erdös
Posté par kantien . Évalué à 2 (+0/-0).
C'est parce que d'une part la philosophie en terminale est une particularité française et que d'autre part c'est incomprhénsible pour une élève de terminale. Si tu lis l'article de Martin-Lof, il explique par exemple que sa déduction des catégories est identique dans le principe à ce que les mathématiciens appellent la correspondance de Curry-Howard.
Les mathématiciens sont plus raisonnables dans la formation de la jeunesse. Personnellement, ce résultat mathématique m'a été enseigné quand j'étais en DEA (Bac +5) : je me suis dit cool, c'est comme Kant mais en plus simple. J'avais justement choisi un DEA en logique mathématique et fondement de l'informatique pour approfondir ma connaissance de la logique et mieux comprendre certains point de la Critique qui me restait obscur.
C'est comme si on disait à un élève de terminale en cours de maths : aujourd'hui on va étudier le théorème d'incomplétude de Gödel et le problème de l'arrêt de Turing, ainsi que leur incidence sur le fondement des mathématiques. Tu penses que ça se passerait bien ?
Ajoute à cela, que les enseignants de philosophie de terminale ne comprennent pas l'ouvrage eux même (Mr Phi en est le parfait exemple) et tu as le parfait cocktail pour du grand n'importe quoi.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Au-delà du problème de Erdös
Posté par serol (site web personnel) . Évalué à 1 (+0/-0).
Quel genre d’enseignement de la philosophie te paraîtrait meilleur ? Pas de philosophie du tout dans l’enseignement secondaire ? Au contraire, un enseignement beaucoup plus progressif étalé sur plusieurs années de lycée voire de collège ou d’école primaire ? Un enseignement moins centré sur la découverte de textes classiques et davantage sur la réflexion logique ou la découverte spontanée de questions philosophiques ? …
[^] # Re: Au-delà du problème de Erdös
Posté par Pol' uX (site web personnel) . Évalué à 2 (+0/-0).
Perso mon expérience (terminale S en 2000-2001) : je croyais qu'on allait « penser ensemble » et que ça serait chouette. En fait non on a bachoté autour de raisonnements, souvent fallacieux, sans même chercher à les déconstruire, avec un prof qui avait lui même du mal à s'y impliquer de façon convaincante. (« Bonjour monsieur, j'ai toujours pas compris pourquoi un pot de fleurs posé sur une table dans un rêve évoque à Freud une connotation sexuelle ? » Depuis j'ai compris sans nul doute que le soucis était chez l'auteur…)
Adhérer à l'April, ça vous tente ?
[^] # Re: Au-delà du problème de Erdös
Posté par kantien . Évalué à 2 (+0/-0).
J'ai eu la même expérience mais un peu plus tôt (96-97) et j'ai eu 5 au bac. :-P
Je me méfie toujours des philosophes, il y a de l'excellent comme du pur AI slop dans cette discipline. Je suis né mathématicien, j'ai vécu en mathématicien et je mourrai en mathématicien. Je suis kantien car, de tous les philosophes que j'ai lu, c'est le seul dont j'ai pu dire « nul ne peut entrer ici, s'il n'est géomètre ». ;-)
Peut-être ce passage de la préface de la deuxième édition te semblera moins chiante à lire :
Et pour avoir lu toute son œuvre, ce qu'il entendait par sciences solides, c'était la logique, les mathématiques, la physique… et la métaphysique qu'il s'est efforcé de fonder. ;-)
Après, mon parcours, c'est classe prépa MPSI-MP, licences de mathématique fondamentale, maîtrise de mathématique pure et DEA de logique. C'est en licence que j'ai découvert la Critique pour les mêmes raisons que David Bessis : comprendre la nature de cette science qui occupe mon esprit en permanence, et ce fût une révélation. C'est uniquement depuis ce temps que je m'intéresse à la philosophie. En DEA, il y avait des étudiants issus soit d'un cursus mathématique (comme moi), soit d'un cursus philosophique (ils galéraient un peu sur certains sujets mathématiques, mais nos discussions étaient des plus rafraîchissante).
Cela étant son œuvre ne se limite pas à ce que l'on appelle de nos jours les sciences « dures », il a eu une influence non négligeable sur l'existence d'institutions comme la Sociétés des Nations, l'Organisation des Nations Unies ou encore l'Union Européenne (voir son opuscule Vers la paix perpétuelle). Il a appliqué le même principe que Curry-Howard au domaine du droit et, dans les facultés de droit ou de sciences politiques, il est étudié pour cela. À la question : pourquoi faut-il trois pouvoirs (le législatif, l'exécutif et le judiciaire) ? il répond que c'est nécessaire conformément à la structure formelle d'un syllogisme :
à la majeure correspond la Loi (le pouvoir législatif), à la mineure correspond le cas ou question de fait dans un procès (le pouvoir exécutif représenté par le procureur) et enfin le juge (pouvoir judiciaire) subsume la mineure sous la majeure pour tirer la conclusion ou sentence.
Et ce qui est drôle, c'est que si l'on regarde un code informatique qui gère des permissions (via Curry-Howard), il suit le même schéma : c'est un tel syllogisme. ;-)
À la question : pourquoi tous les hommes naissent-ils libre et égaux en droit ? Il répond que c'est l'équivalent juridique du principe d'action-réaction chez Newton, et que ces deux principes ont pour fondement la forme logique des jugements disjonctifs (A ou B).
Et là on sort totalement du cadre légitime du recours à la méthode axiomatique (limitée aux mathématiques), mais la structure formelle reste identique : voilà, pour moi, l'essence de ce que Kant a apporté à la philosophie. ;-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Au-delà du problème de Erdös
Posté par kantien . Évalué à 2 (+0/-0).
Comme le montre mon commentaire en réponse à Polux, je n'ai rien à préconisé pour l'enseignement de la philosophie. Je suis avant tout mathématicien et la philosophie fut pour moi nécessaire pour répondre à mes problèmes. Je laisse aux philosophes des académies le soin d'orchestrer leur enseignement comme ils l'entendent. ;-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Au-delà du problème de Erdös
Posté par serol (site web personnel) . Évalué à 1 (+0/-0).
Le contenu de l’enseignement de la philosophie ne dépend pas seulement de ce que veulent les philosophes et les professeurs de philosophie, mais aussi de l’importance que la société confère à cet enseignement.
La valeur qu’attribue notre société aux mathématiques est telle que treize ans d’enseignement minimum lui sont consacrés (de l’âge de 3 ans à celui de 16 ans), contre seulement un an pour la philosophie (et ce seulement pour les jeunes qui passent un bac général, soit environ 45 % d’une génération).
13 ans d’étude minimum (et jusque 20 ans d’étude dans le cas de l’obtention de certains masters scientifiques), ça laisse un peu de temps pour organiser un enseignement « raisonnable ».
Pour revenir à la découverte de la pensée de Kant en classe de terminale : je me dis que les professeurs de philosophie sont dans une situation assez difficile. D’un côté : comment réussir à faire découvrir correctement la complexité de la pensée de Kant pendant cette seule année d’enseignement de la philosophie ? D’un autre côté : est-il possible de ne pas aborder ce classique des classiques pendant ce cours de philosophie qui sera probablement le seul de la vie de ces jeunes ?
[^] # Re: Au-delà du problème de Erdös
Posté par kantien . Évalué à 2 (+0/-0).
Je sais bien les contraintes auxquelles ils doivent faire face, ce que je voulais dire dans mon précèdent message est que je ne me sens pas légitime pour leur donner le moindre conseil.
Une idée qui me vient à l'esprit, et qui pourrait profiter au philosophe, est une proposition faîte par Gérard Huet dans un conférence intitulée Fondements de l'informatique, à la croisée des mathématiques, de la logique et de la linguistique (le document est un
docxmais il s'ouvre bien avec libre office). Il illustre par deux exemple comment on pourrait faire mettre en pratique ce qui se cache dans Curry-Howard (et donc la logique transcendentale de Kant) sans nécessairement aborder la théorie elle-même (au fond ce qu'expose ces théories est la structure logique de notre esprit, mais cette structure on l'utilise naturellement sans même savoir l'exposer théoriquement).Les exemples se trouvent à la fin de sa conférence (dans ma version que j'ai convertie en
pdf, c'est à la page 20) est commence au paragraphe :Le premier exemple consiste à calculer le coût financier du cycle de lavage d'une machine à laver, puis à réfléchir sur le raisonnement qui conduit à la réponse. Si Luc Skywalker me lit, c'est analogue à la discussion que tu as eu avec gUI sur la rentabilité de récupérer l'énergie potentiel sur un vélo électrique : vous avez utilisé la Critique de la raison pure sans le savoir (catégorie de la causalité dans la logique transcendentale). ;-)
Le second consiste à faire de l'analyse grammaticale sur les verbes transitifs et intransitifs, avec pour exemple « le chat mange la souris ».
Puis de montrer que, d'un certain point de vue, les deux situations sont identiques dans notre manière de raisonner.
Pour répondre à cette question :
Je dirais absolument oui, il l'a dit lui-même !
Sans entrer dans le détail de son œuvre, je vais juste illustrer pourquoi je dis de lui « nul ne peut entre ici s'il n'est géomètre ». Les géomètres, ou plus généralement les mathématiciens, utilisent pour résoudre leur problème une méthode qu'ils nomment le raisonnement par analyse-synthèse. Pappus d'Alexandrie le décrivait en ces termes :
Dans l'analyse on va de la conclusion aux prémisses, tandis que dans la synthèse on redescend des prémisses à la conclusion. D'ailleurs, le logiciel d'aide à la preuve Rocq fonctionne ainsi : on prouve la proposition par voie d'analyse, puis, quand on a fini, on écrit
qed(quod erat demonstrandum ou cqfd) et le moteur de Rocq effectue la synthèse pour nous.Je me suis permis cette petite digression parce que certains ouvrages de Kant vont par paire : dans l'un il suit la voie analytique, dans l'autre la voie synthétique. Dans le cas de la Critique de la raison pure, c'est la voie synthétique qui est suivie. Son ouvrage jumeau, qui suit la voie analytique, se nomme les prolégomènes à toute métaphysique future. Ce dernier s'ouvre sur cette avertissement (première phrase de la préface) :
Ils servent à exposer la voie de découverte (la méthode analytique est la voie de la recherche qui trouve) qui mène à la Critique (dont l'exposé est synthétique).
Partant de là, je doute fort, tout de même, qu'il soit approprier d'aborder cet ouvrage avec des élèves de terminal sans finir dans du n'importe quoi, d'autant que, je le répète, un professeur de terminal ne le comprend peut être pas lui-même.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Au-delà du problème de Erdös
Posté par serol (site web personnel) . Évalué à 1 (+0/-0).
Merci pour ta longue réponse. Je te lis, comme souvent, avec attention et intérêt.
[^] # Re: Au-delà du problème de Erdös
Posté par kantien . Évalué à 2 (+0/-0).
Après reflexion, j'ai oublié un point. Si les professeurs de philosophie sont sans doute tenter d'aborder l'ouvrage c'est à cause de la notion de liberté, qu'il leur faut traiter dans leur programme.
Si le synthétique a priori mène à des questions sans réponses en mathématique, les propositions indécidables de Gödel et Turing, il en est de même pour le synthétique a priori en philosophie. Chez Kant cela se nomme les antinomies de la raison pure et, comme pour les mathématiques, cela se produit lorsque l'on introduit la récursivité. La plus célèbre de ces antinomies étant la troisième, connue sous sa forme populaire du problème de l'œuf et de la poule, et la réponse de Kant à la question de savoir qui vient en premier est de dire : ni l'un, ni l'autre mais l'homme est libre. :-D
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Au-delà du problème de Erdös
Posté par Luc-Skywalker . Évalué à 2 (+0/-0).
Disons que potasser Kant tout au long de l'année alors que tu n'y comprends pas grand chose, c'était pas cool.
Le reste du cours de Philo était plutôt intéressant par contre. Au Bac, j'ai pris le sujet de dissertation sur la Liberté et j'ai eu 15 je crois.
Donc, ça c'est bien passé quand même ;)
"Si tous les cons volaient, il ferait nuit" F. Dard
[^] # Re: Au-delà du problème de Erdös
Posté par Pol' uX (site web personnel) . Évalué à 2 (+0/-0).
Il répond ça où, stp ?
Adhérer à l'April, ça vous tente ?
[^] # Re: Au-delà du problème de Erdös
Posté par kantien . Évalué à 2 (+0/-0).
Dans la Critique de la Raison pure au chapitre sur la méthodologie :
Il faut lire la suite aussi, où il explique qu'au sens propre du terme seule la mathématique possède des définitions, raisons pour laquelle les BA des LLM ne savent même pas ce qu'ils demandent lorsqu'ils exigent une définition de l'intelligence. Mais bon, ce sont des adeptes de la métaphysique de bistro. ;-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Au-delà du problème de Erdös
Posté par Pol' uX (site web personnel) . Évalué à 2 (+0/-0).
Merci. Même si je ne te cache pas que je trouve ça chiant à lire. :)
Adhérer à l'April, ça vous tente ?
Envoyer un commentaire
Suivre le flux des commentaires
Note : les commentaires appartiennent à celles et ceux qui les ont postés. Nous n’en sommes pas responsables.