Les vérificateurs de preuves et le copilote mathématique IA selon Terence Tao
(scientificamerican.com)- À mesure que les démonstrations mathématiques sont formalisées de façon plus rigoureuse, des outils comme Lean vérifient les preuves humaines et transforment la base de confiance des collaborations à grande échelle
- Avec l’accumulation de bibliothèques standard comme mathlib, le seuil d’entrée pour formaliser des théorèmes de niveau licence comme de nouveaux domaines est en train de baisser
- Lors de la formalisation de la conjecture PFR, plus de 20 participants se sont réparti de petites étapes de preuve, et Terence Tao s’est concentré sur l’orientation générale plutôt que sur une relecture ligne par ligne
- L’IA est moins proche de “résoudre” les mathématiques à court terme que de jouer le rôle d’un copilote de preuve, en aidant à la formalisation, à la vérification et au travail itératif
- La recherche mathématique pourrait évoluer vers des tâches plus explicites et davantage réparties entre humains : définition de la direction, formalisation détaillée, entraînement de l’IA et interprétation des preuves générées par l’IA
La formalisation transforme la collaboration mathématique
- La recherche mathématique traditionnelle relevait plutôt de petites collaborations, et Tao estime en général qu’environ 5 personnes représentent une limite haute raisonnable
- Avec un vérificateur automatique de preuves, il devient possible de collaborer avec des centaines de personnes qui ne se connaissent pas
- Les contributeurs soumettent du code, et le compilateur Lean le vérifie
- La confiance ne dépend plus uniquement des relations personnelles, elle peut être confirmée par le résultat de la vérification formelle
- Lors de la formalisation d’un résultat récent sur la conjecture Polynomial Freiman-Ruzsa (PFR), plus de 20 personnes ont participé
- La preuve a été découpée en un grand nombre de petites étapes
- Chaque participant a pris en charge la preuve d’une étape
- Tao a surtout piloté la direction d’ensemble plutôt que de vérifier chaque contribution ligne par ligne
Tous les mathématiciens n’ont pas besoin d’être programmeurs
- Dans un projet de formalisation, il est possible de répartir les rôles
- Certains se concentrent sur la direction mathématique
- D’autres se spécialisent dans la transformation de petits fragments mathématiques en preuves formelles
- Même des mathématiciens peu familiers avec l’informatique, comme Peter Scholze, peuvent participer à des projets Lean
- Lorsqu’un grand problème mathématique est découpé en petits morceaux, on peut contribuer à une sous-tâche précise sans comprendre toute la théorie
Lean, mathlib et la recherche rendent tout cela plus pratique
- L’une des principales raisons pour lesquelles les mathématiques formelles deviennent réellement utilisables est le progrès des bibliothèques mathématiques standard
- Lean dispose d’un vaste projet appelé mathlib
- Des théorèmes fondamentaux de niveau licence, en calcul différentiel ou en topologie par exemple, y sont ajoutés un à un
- L’objectif est d’amener la bibliothèque jusqu’au niveau master et doctorat
- Cela rendrait ensuite la formalisation de nouveaux domaines mathématiques plus facile
- Pour construire une preuve, il faut retrouver des théorèmes déjà établis comme vrais, ce qui rend aussi importants des moteurs de recherche plus intelligents
- Une fois tout le projet PFR formalisé, la compilation de vérification ne prend qu’environ 30 minutes
- Le goulot d’étranglement n’est pas tant la puissance de calcul que l’utilisabilité, la convivialité et l’adaptation des personnes à ces outils
- Lean est aujourd’hui considéré comme le langage formel à la communauté la plus active
- Pour des projets en auteur unique, d’autres langages peuvent être plus adaptés
- Lean est relativement facile à apprendre, avec une bonne bibliothèque et une bonne communauté
- Il pourra peut-être être remplacé plus tard par une autre option, mais c’est aujourd’hui le langage formel dominant
Un coût de formalisation encore élevé
- Tao estime qu’il pourrait formaliser certains projets, mais qu’aujourd’hui cela pourrait lui coûter un mois de son temps
- On n’est pas encore au stade où tous les résultats seraient formalisés au quotidien
- Quand cela aide à apprendre Lean
- Quand l’exactitude du résultat est particulièrement importante
- Il faut choisir des projets pour lesquels la formalisation apporte une vraie valeur
- À mesure que la technologie progresse, le coût de la formalisation pourrait diminuer
- Aujourd’hui, cela peut prendre 10 fois plus de temps que les méthodes classiques
- À l’avenir, ce surcoût pourrait tomber à 2 fois, voire à moins d’1 fois
L’IA peut devenir le copilote du mathématicien
- Tao imagine un futur où, au lieu de taper directement une preuve, le mathématicien l’explique à un système comme GPT, pendant que l’IA tente en parallèle une formalisation sous Lean
- Si la vérification passe, on pourrait fournir à la fois l’article en LaTeX et la preuve Lean
- Si l’utilisateur le souhaite, l’assistant pourrait même aider jusqu’à la soumission à une revue
- Aujourd’hui, la voie la plus rapide vers la formalisation reste encore qu’un humain produise d’abord l’idée et l’ébauche de la preuve
- À long terme, on peut imaginer des projets où aucun humain ne connaît toute la preuve, mais où de petits fragments sont formalisés puis reliés par des humains et des IA pour démontrer un grand théorème
- Tao pense qu’il faudra plusieurs années pour en arriver là
- Les technologies actuelles restent insuffisantes et la formalisation demeure un travail pénible
Loin des prédictions selon lesquelles « les mathématiques seraient résolues »
- Tony Wu et Christian Szegedy ont affirmé qu’en 2 à 3 ans, les machines trouveraient des preuves mieux que les humains, au point que les mathématiques seraient “résolues” en ce sens
- Tao pense qu’en 3 ans, l’IA pourrait devenir utile aux mathématiciens et produire des avancées nettes, mais pas que les mathématiques seraient résolues
- L’IA peut devenir un copilote quand une étape d’une preuve semble vraie sans que l’humain voie immédiatement pourquoi
- Même si l’IA atteint le niveau actuel des humains en mathématiques, les mathématiciens pourront se déplacer vers un niveau plus élevé
- Il pourrait aussi devenir possible de démontrer des centaines ou des milliers de théorèmes d’un coup grâce à l’IA
- Les mathématiciens humains joueraient alors un rôle de direction sur ce que l’IA doit faire
- Tao juge toutefois un calendrier de 2 à 3 ans quelque peu agressif pour un tel changement
Comprendre les preuves et les preuves générées par l’IA
- Une preuve mathématique n’est pas seulement une procédure de vérification de vérité, c’est aussi une manière de comprendre pourquoi c’est vrai
- Dans un avenir proche, l’IA automatisera surtout les tâches fastidieuses et triviales, tandis que les humains garderont probablement le rôle de direction
- Si l’IA produit une preuve difficile à comprendre et peu élégante, les humains pourront l’analyser à nouveau
- Par exemple, dans une preuve qui tire une conclusion à partir de 10 hypothèses, on peut vérifier si l’une d’elles peut être supprimée sans invalider le résultat
- Un nouveau type de mathématicien pourrait émerger, spécialisé dans l’extraction d’intuition à partir des preuves générées par l’IA
- Les premières preuves d’IA peuvent sembler dépourvues d’intuition
- Les humains pourront les rendre plus compréhensibles et en dégager la structure
Problèmes non résolus et limites de l’IA
- Pour prouver une conjecture non résolue, il faut d’abord pouvoir la découper en morceaux plus petits
- Transformer un problème en un problème plus difficile est bien plus facile que le réduire à un problème plus simple
- Tao estime que l’IA n’a pas encore montré qu’elle était meilleure que les humains pour ce travail de décomposition
- L’idée d’utiliser l’IA pour suggérer des connexions possibles entre plusieurs domaines est intéressante
- Le taux de réussite reste aujourd’hui faible
- Sur 10 suggestions, une seule peut être intéressante et les 9 autres inutiles
- Tao pense toutefois que cela pourrait évoluer à l’avenir
Le problème des données pour la connaissance mathématique
- L’un des problèmes de l’entraînement des IA mathématiques est le manque de données suffisantes
- Les articles disponibles en ligne peuvent servir à l’entraînement, mais une grande partie de l’intuition mathématique n’y figure pas
- Les conversations entre mathématiciens
- Les cours
- La manière d’encadrer les étudiants
- Les tentatives ratées et le processus de correction
- Les preuves publiées sont des résultats compressés, et les gens ont tendance à ne publier que les réussites
- Les données les plus précieuses sont en réalité celles qui montrent ce qui a été tenté, ce qui n’a pas marché et comment cela a été corrigé
- À l’avenir, les tentatives de recherche et les échecs pourraient être enregistrés pour entraîner l’IA ou éviter à d’autres chercheurs de répéter les mêmes impasses
- Tao donne l’exemple d’une situation où l’on accepterait d’enregistrer son processus de recherche pour pouvoir utiliser, en 2040, un système avancé de type AI Lean
Vers des mathématiques plus explicites
- Une grande partie du savoir mathématique reste enfermée dans la tête des mathématiciens, et seule une très petite part est explicitement consignée
- Plus la formalisation progresse, plus le savoir implicite se transforme en savoir explicite
- Des manuels formalisés pourraient déboucher sur des manuels interactifs
- On commencerait par une explication de haut niveau de la preuve
- Si une étape n’est pas comprise, on pourrait l’ouvrir à un niveau de détail supérieur
- Et si on le souhaite, on pourrait descendre jusqu’au niveau des axiomes
- Cette approche pourrait permettre à des mathématiciens d’un domaine de contribuer plus facilement à un autre
- Les sous-tâches d’un grand projet peuvent être spécifiées avec précision
- Il devient possible de participer à la partie nécessaire sans comprendre l’ensemble
1 commentaires
Commentaires Hacker News
https://archive.is/Idouw
L’expression project manager mathematicians rappelle le texte satirique “A letter to my old friend Jonathan” [1], écrit par Edsger Dijkstra en 1975, ainsi que son texte de suivi [2]
C’était un texte critique qui montrait à quel point il serait absurde d’appliquer à la mathématique la façon dont on fabrique du logiciel, mais, d’une certaine manière, il était visionnaire
Le cœur du propos était de critiquer l’absurdité de l’application de droits de propriété intellectuelle, en particulier aux vérités mathématiques ; heureusement, avec la vague actuelle de mécanisation, cet aspect ne semble pas être une grande source d’inquiétude
[1]: https://www.cs.utexas.edu/users/EWD/transcriptions/EWD04xx/E...
[2]: https://www.cs.utexas.edu/users/EWD/transcriptions/EWD05xx/E...
C’est un billet perspicace, mais il me semble qu’il manque le fait que les LLM abstraient de plus en plus de façon surhumaine
Tao dit qu’« il est facile de transformer un problème en problème plus difficile, mais difficile de le rendre plus simple, et l’IA n’a jamais montré qu’elle faisait mieux que les humains sur ce point » ; pourtant, le mode de fonctionnement des LLM pourrait permettre un niveau de compréhension bien plus élevé
Aujourd’hui, ils ressemblent surtout à des assistants, des vérificateurs de faits et des exécutants de tâches ennuyeuses, mais ils proposeront bientôt des intuitions. Les LLM compressent déjà des embeddings et des connaissances, et possèdent des intuitions que nous ne voyons pas
Le passage où Hinton prend l’exemple du lien entre une bombe nucléaire et un tas de compost : https://www.youtube.com/watch?v=Gg-w_n9NJIE&t=4613s
Ce sont seulement des machines entraînées à imiter la manière dont les humains écrivent, et il n’existe pas de données d’entraînement nécessaires pour imiter quelque chose de plus intelligent que les humains
Je ne doute pas que le machine learning dépassera l’intelligence humaine, mais le goulet d’étranglement consiste à trouver comment le faire apprendre par lui-même à partir de ses propres sorties, sans intervention humaine, plutôt que de régresser sur l’ensemble des textes du monde
Ramanujan a fait de brillantes découvertes mathématiques sans formation formelle et avec seulement quelques livres de mathématiques à sa disposition ; du point de vue des données d’entraînement d’un modèle de machine learning, c’est une quantité presque négligeable
Il m’a fallu une dizaine de secondes pour le formuler avec des mots, mais quand on connaît les informations nécessaires, la réponse est évidente
Hinton dit que cela montre une pensée analogique, mais il existe en ligne beaucoup de textes sur le jardinage et sur la physique des tas de compost, et il est tout à fait possible que ChatGPT les ait déjà vus pendant son entraînement
Cet exemple ressemble donc à un cas où l’on ne contrôle pas le fait que le LLM ait, en pratique, déjà vu la réponse dans les textes d’entraînement
Le passage plus loin dans la vidéo où Ilya dit « il existe une preuve d’existence : le cerveau humain est un réseau de neurones » (https://youtu.be/Gg-w_n9NJIE?t=4966) est lui aussi intéressant. Je suis globalement d’accord avec l’idée que le cerveau humain est aussi un réseau de neurones, mais il y a aussi beaucoup de contre-arguments, notamment le fait que les vrais neurones ne fonctionnent pas en 8 bits et que les types de cellules, l’ADN et l’environnement chimique hormonal sont différents ; j’y vois donc un embranchement philosophique
Cela peut se faire en quelques minutes à quelques heures
À l’inverse, pour obtenir un expert humain de plus, il faut qu’apparaisse quelqu’un qui aime suffisamment les mathématiques pour en faire son métier, qu’il suive des décennies de formation et de spécialisation avancée, sans garantie qu’il aille jusqu’au bout ni qu’il atteigne le niveau nécessaire pour repousser la frontière des connaissances
Pendant qu’on attend tout ce temps, on pourrait créer des milliers de milliards d’experts IA fonctionnant en parallèle
La bande passante avec laquelle le cerveau humain absorbe de nouvelles informations est faible, mais les machines peuvent répliquer en quelques secondes les connaissances d’une vie, mener des milliers de conversations en parallèle, et même sérialiser une partie d’un cerveau pour l’envoyer à une autre IA. Si l’on va jusqu’à la matière programmable, on pourrait fabriquer du computronium à un rythme exponentiel, et atteindre une sorte de point Oméga où des millénaires de recherche seraient accomplis en quelques secondes
Je ne connais absolument rien aux mathématiques, mais cela me rappelle l’histoire du logiciel. Autrefois, des projets incroyables comme RollerCoaster Tycoon étaient presque l’œuvre d’une seule personne
Ensuite, l’ingénierie logicielle s’est modularisée d’une manière assez proche de ce qui est décrit dans l’interview, et aujourd’hui c’est devenu une immense chaîne d’assemblage où des gens comme moi produisent du React pour gagner leur vie ; la productivité par personne, ou le niveau de compétence requis, semble être tombé presque à 0
J’ai l’impression que, quand un domaine est à son apogée, un génie garde cent choses en tête et réalise le meilleur travail, puis quand cela est remplacé par une chaîne d’assemblage, ce domaine cesse de produire des choses réellement précieuses
L’ingénierie logicielle n’a pas cessé de faire des choses remarquables ; je pense même que c’est tout le contraire
Blague à part, le jour où il faudra corriger un bug critique, les compétences se verront. Le fait qu’un produit ou un service soit devenu stable et rentable ne signifie pas que les développeurs d’origine sont partis, ni que plus personne ne peut accomplir de grandes choses
Dire que ce domaine ne crée plus rien de vraiment précieux est profondément faux
C’est comme comparer une cathédrale construite par 100 personnes en 100 ans à une cabane construite par une seule personne en un mois. La cabane tient debout et offre un toit, mais ce n’est pas une cathédrale
Côté développement web, rien qu’en essayant de suivre Python, il y a tellement de frameworks et de technologies pour chaque petit rouage de la machine qu’il est vraiment difficile de suivre
Les compétences suivent en général une distribution log-normale, donc les personnes exceptionnelles sont rares par nature ; dans un petit domaine naissant, le manque d’infrastructure de support peut faire que seules les personnes extrêmement talentueuses survivent, ce qui donne une densité irréaliste de talents de tout premier plan
Bricoler de force 47 frameworks récents pour sortir une application de liste de tâches est fondamentalement différent de produire un impact significatif
Du point de vue coût-bénéfice, il existe un optimum local fort qui consiste à cracher beaucoup de code à bas coût plutôt qu’à investir longtemps dans de grands projets ; à mesure qu’un domaine mûrit, le seuil minimal de compétence pour atteindre ce point baisse
Peu d’organisations se concentrent sur la formation de talents de tout premier plan. Il est donc facile d’expliquer pourquoi, quand un domaine grossit, le niveau moyen baisse s’il est laissé à lui-même ; et si l’on gère mal la distribution, cela peut coûter cher à corriger plus tard
Les preuves vérifiées par ordinateur sont un domaine où l’IA pourrait devenir utile assez vite. Cela dit, elles pourraient ressembler davantage au réseau neuronal d’un moteur d’échecs qu’à un LLM complet
Tout prouver à la main est ennuyeux et prend beaucoup de temps, et on utilise déjà beaucoup de solveurs, mais les tactiques ou les solveurs peinent lorsqu’on leur fournit trop de théorèmes et de lemmes
Un réseau neuronal servant de moteur de recherche pour retrouver par correspondance de motifs les lemmes pertinents convient bien
L’induction et l’unification d’ordre supérieur relèvent elles aussi, en pratique, de la synthèse de code, et énumérer brutalement tous les arbres syntaxiques possibles est très inefficace
Les solveurs font de toute façon du backtracking, donc ce n’est pas grave si l’IA propose des lemmes inutiles à 95 %, et cela pourrait être spectaculairement meilleur que la recherche manuelle
En revanche, je ne suis pas sûr que les preuves vérifiées par ordinateur soient forcément bonnes pour la communication. Les preuves destinées aux humains sont de haut niveau et omettent des détails pour d’autres raisons que leur simple longueur
Le problème central est qu’il faut les relier aux définitions formelles des objets mathématiques utilisés dans la preuve
Mais ce n’est pas ainsi que les humains pensent lorsqu’ils écrivent ou lisent une preuve. En général, on a une intuition informelle de haut niveau de ce que l’on fait « moralement », puis on complète les détails formels autant que nécessaire
Le code informatique fonctionne dans une certaine mesure parce que la sémantique formelle du langage est beaucoup plus proche du modèle mental, mais en mathématiques les objectifs sont généralement différents
La stratégie sledgehammer d’Isabelle combine des démonstrateurs automatiques de théorèmes comme E, Z3, SPASS et Vampire pour tenter de prouver ou de réfuter un objectif
En théorie, cela paraît correct, mais en pratique on obtient une preuve reconstruite qui applique une douzaine de lemmes apparemment arbitraires ; ce type de preuve est illisible et très fragile
Il ne me semble pas que l’IA va résoudre ce problème par magie
Les réseaux neuronaux actuels ont une efficacité d’échantillonnage extrêmement faible, et les jeux de données de mathématiques formelles sont bien plus petits que des jeux de données comme du code Python
Terence Tao a donné il y a quelques mois une excellente conférence sur ce sujet, qui traite plus en détail de l’utilisation de Lean : https://www.youtube.com/watch?v=AayZuuDDKP0
Un mathématicien en activité dit avoir fait démontrer par GPT-4o, dans le cadre de ses recherches, ce qui est probablement un nouveau lemme
« Mon partenaire est mathématicien et, la semaine dernière, il a utilisé ChatGPT pour la première fois afin de démontrer quelques lemmes pour ses recherches. Il soupçonnait déjà que ces résultats étaient vrais et avait aussi une idée générale de l’approche, mais il n’était pas spécialiste de ce type d’énoncés. C’était la première fois qu’il obtenait du modèle une preuve correcte et utile
Le premier lemme avait été repéré par un collaborateur dans des calculs pour de petites valeurs de e. ChatGPT n’a pas trouvé de preuve avant qu’on lui suggère d’essayer avec la fonction de Möbius
https://chatgpt.com/share/9ee33e31-7cec-4847-92e4-eebb48d4ff...
Le second semble plus standard, et Mathematica aurait probablement pu le faire aussi. Mais Mathematica ne donne pas de dérivation propre, donc cela reste utile
https://chatgpt.com/share/7335f11d-f7c0-4093-a761-1090a21579... »
Ces systèmes deviennent effrayamment bons en raisonnement et sur des sujets difficiles
Si le domaine du machine learning continue à se concentrer sur l’ajout de capacités de système 2 pour compléter la pensée de système 1, dont les LLM sont à peu près l’équivalent, les choses risquent de devenir mouvementées
C’est une mémoire impressionnante, pas un raisonnement nouveau
Nous l’avons vu comme une somme sur les partitions ordonnées, plutôt qu’une somme sur des partitions avec un coefficient |τ|!, mais les deux sont évidemment la même chose
Si l’on prend des partitions ordonnées cycliquement, c’est-à-dire avec un coefficient (|τ|-1)! au lieu de |τ|!, on obtient 0 plutôt que (-1)^e
La preuve combinatoire de Beren consiste à choisir un élément spécial et à construire une bijection entre les partitions cycliquement ordonnées de longueur paire et impaire : si cet élément est seul, on le fusionne avec la partie suivante ; s’il ne l’est pas, on le sépare dans sa propre partie
Dans le cas d’un ordre linéaire, on applique une méthode similaire à partir du dernier élément, mais les partitions où le dernier élément est seul dans la dernière partie ne sont pas appariées, donc on continue récursivement avec l’élément suivant
Au final, tout est apparié, et il ne reste que la partition où tous les éléments sont séparés et dans l’ordre d’origine. Selon la parité de la taille de l’ensemble initial, la somme signée donne l’énoncé de départ
On ne sait même pas combien de termes contient la somme sur « τ ≤ τ », et le lien avec le fait d’établir un des côtés gauche ou droit de l’étape 3 puis d’en déduire l’autre ne tient pas
En réalité, ChatGPT s’est souvenu de la fonction de Möbius du treillis des partitions et l’a récitée sans preuve, puis a produit ensuite un charabia seulement plausible en surface
Or établir cette fonction de Möbius est en fait le cœur du problème, et la question revient presque à demander de démontrer que cette fonction a cette forme
De plus, la formule générale donnée par ChatGPT est légèrement fausse, et elle n’est correcte que dans le cas |σ| = 1, qui est le cas important pour la preuve en cours
Ce fait se voit immédiatement, sans utiliser explicitement tout l’appareil des fonctions de Möbius, en posant N(t,e) comme le nombre de partitions en t classes d’équivalence et en faisant une induction élémentaire avec la récurrence N(t,e+1)=N(t-1,e)+tN(t,e)
Trois points ressortent de cette interview
Premièrement, Tao parle de project manager mathematicians et imagine un futur où l’intuition mathématique serait « produite » comme d’autres productions de la société. Il explique que si les mathématiques n’ont pas encore été industrialisées ainsi, c’est à cause d’un manque d’outils, et il voit l’IA et les assistants de preuve comme potentiellement révolutionnaires sur ce point. L’interaction et le guidage humains restent toutefois nécessaires
Deuxièmement, il existe énormément de connaissances tacites qui ne figurent pas dans les articles. Les intuitions ou la connaissance des échecs sont importantes, au point que même les meilleurs mathématiciens doivent se parler pour éviter de répéter les mêmes erreurs
Troisièmement, on peut facilement croire que les mathématiques sont déjà suffisamment formalisées, mais les articles présupposent beaucoup de savoir commun. Formaliser les preuves d’une manière compréhensible par des assistants de preuve aide davantage de personnes à comprendre ce qui se passe réellement
Comme Tao l’a montré dans ses conférences sur le projet Polymath, il apparaît clairement comme quelqu’un qui cherche toujours de nouvelles façons de faire de la recherche mathématique
Pour l’instant, ce type de projet est peut-être envisageable quand des médaillés Fields comme Tao ou Scholze ont la marge nécessaire pour consacrer 10 fois plus de temps aux preuves
J’ai récemment discuté avec un postdoctorant d’un département de mathématiques de tout premier plan, et il disait que personne autour de lui n’utilisait lean4 dans son travail réel
Pour un chercheur en début de carrière, il vaut sans doute mieux faire confiance à son intuition et publier l’article
Pour juger correctement ce sujet, les impressions de quelques personnes ne suffisent pas
À l’inverse, dans des domaines au style plus intuitif, comme la topologie de basse dimension, je m’attendrais à ce que moins de gens utilisent des vérificateurs de preuve
Ici, intuitif ne veut pas dire moins rigoureux. Une preuve par dessin d’une équivalence d’homotopie est bien plus difficile à traduire pour que Lean puisse la comprendre qu’une liste d’inégalités
Pour ma part, je suis du côté géométrie/topologie, et je n’ai encore jamais vu ni entendu parler de personnes utilisant ces outils
https://lean-lang.org/
https://github.com/leanprover/lean4
Le passage selon lequel « si l’IA fournit une preuve incompréhensible et laide, on peut l’analyser. Si cette preuve utilise 10 hypothèses pour obtenir une conclusion, la preuve fonctionne-t-elle encore si l’on supprime une hypothèse ? Cette science n’existe pas encore, faute de nombreuses preuves générées par IA, mais un nouveau type de mathématicien apparaîtra pour prendre des mathématiques générées par IA et les rendre plus compréhensibles » correspond exactement à ce que je pense de la conception d’API publiques dans le code
Un rôle traditionnellement réservé aux développeurs expérimentés pourrait désormais être largement simplifié et devenir accessible à tous