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.
# Au-delà du problème de Erdös
Posté par kantien . En réponse au lien Commentaire de gro-tsen sur la vidéo de Mr phi sur la résolution par LLM du problème de la distance unitaire. Évalué à 5 (+3/-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.