Voici une question importante à laquelle nous devons de plus en plus faire face à mesure que les pipelines d'IA pour les mathématiques deviennent plus courants : Pourquoi nous soucions-nous de résoudre des problèmes difficiles ? Presque toujours, la réponse n'est *pas* que nous voulons particulièrement que le problème difficile soit résolu. (1/12)

Des questions comme l'existence de solutions globalement lisses aux équations de Navier-Stokes suscitent un intérêt mathématique non pas parce que la réponse elle-même est terriblement importante, mais parce que nous avons des raisons de croire que le processus de *découverte* de la réponse est très probablement... (2/12)

...pour offrir de nouvelles perspectives profondes sur l'analyse, les EDP, la dynamique des fluides, etc., avec de nouvelles techniques à exploiter. La résolution de Fermat nous a donné (indirectement) le programme de Langlands. La résolution de Poincaré nous a donné l'écoulement de Ricci. On espère que la résolution des équations de Navier-Stokes nous donnera quelque chose d'aussi monumental. (3/12)

En effet, nous identifions de tels problèmes comme étant "intéressamment difficiles" précisément parce que nous intuitons qu'ils représentent un "écart" dans notre compréhension et nos méthodes actuelles. C'est pourquoi les illuminés qui prétendent résoudre (par exemple) l'hypothèse de Riemann en utilisant des "trucs" ou des méthodes élémentaires... (4/12)

...manquent quelque peu le point : si l'un de ces grands problèmes s'avérait soluble en utilisant uniquement les connaissances mathématiques et la technologie existantes, ce serait une immense déception : une source que nous pensions auparavant jaillissante est, en fait, à sec. (5/12)

Quel rapport cela a-t-il avec l'IA ? Eh bien, si l'on accepte le postulat selon lequel les problèmes difficiles sont principalement intéressants en raison des nouvelles perspectives et compréhensions qu'ils apportent, cela soulève la question (à la lumière des développements de l'IA) : qui est responsable de la partie "compréhension" ? (6/12)

Prenons les preuves par épuisement (comme dans le théorème des quatre couleurs), qui ont longtemps été considérées comme quelque peu controversées, car elles fournissent la partie "certitude épistémique" d'une preuve, sans nécessairement livrer aucune des parties "perspicacité" (qui est généralement ce qui nous intéresse) (7/12)

Ainsi, les preuves par épuisement ne sont certainement pas "fausses", mais elles sont en quelque sorte "malhonnêtes", ou peut-être "autodéfaites" : elles ferment un problème potentiellement fructueux, tout en éludant précisément ces aspects des mathématiques qui le rendent intéressant et digne d'être étudié. (8/12)

Je pense que les preuves générées par l'IA, en l'absence de tout niveau de compréhension ou d'insight de la part de l'humain qui les a générées, devraient être considérées de la même manière. Si vous générez automatiquement une preuve Lean d'un grand théorème, c'est super ! Mais pourquoi l'avez-vous fait ? (9/12)

Si vous ne comprenez pas les nouvelles idées/méthodes que contient la preuve, alors tout ce que vous avez fait est de déplacer le fardeau intellectuel de vous-même vers quiconque est prêt à le lire et à le comprendre (et, espérons-le, à communiquer les idées qui y sont contenues à d'autres). (10/12)

Les mathématiques sont finalement un artefact culturel humain (probablement notre plus profond, riche et ancien). Résoudre des problèmes difficiles n'a jamais été censé être qu'un *proxy* pour étendre cet artefact. L'IA rend excitant et facile de générer de nouveaux chemins de compréhension mathématique.. (11/12)

...dans cet artefact, mais cela rend également plus facile que jamais d'atteindre le proxy (c'est-à-dire résoudre des problèmes difficiles), tout en manquant la raison pour laquelle nous nous en soucions au départ (c'est-à-dire approfondir notre compréhension). S'il vous plaît, ne faites pas ça. (12/12)