L’assistance de l’IA devient courante sur le site des problèmes d’Erdős

• Lors de la résolution du problème d’Erdős n°367, les outils d’IA ont joué un rôle central, avec un cas signalé de collaboration entre mathématiciens humains et IA
• Wouter van Doorn a présenté un contre-exemple produit par un humain pour la deuxième partie du problème, puis Gemini Deepthink a généré une preuve complète de la congruence correspondante
• Terence Tao a publié une version simplifiée de la preuve fondée sur la théorie algébrique des nombres p-adiques de Gemini, puis a mentionné la possibilité d’une formalisation dans Lean
• Boris Alexeev a achevé la formalisation dans Lean à l’aide de l’outil Aristotle de Harmonic, en vérifiant manuellement l’énoncé final pour éviter les abus de l’IA
• Cette succession d’étapes montre que l’assistance de l’IA dans la recherche mathématique est progressivement en train de devenir une procédure standard

---

Exemple de collaboration avec l’IA autour du problème d’Erdős n°367

• Le 20 novembre, Wouter van Doorn a présenté un contre-exemple pour la deuxième partie du problème, qui reposait sur l’hypothèse qu’une certaine congruence était vraie
  • Il a demandé aux autres participants de vérifier la validité de cette congruence
• Quelques heures plus tard, Terence Tao a soumis la question à Gemini Deepthink et a obtenu, en une dizaine de minutes, une preuve complète de la congruence ainsi qu’une vérification de l’argument dans son ensemble
  • La preuve de Gemini utilisait la théorie algébrique des nombres p-adiques, et Tao l’a transformée en une preuve élémentaire plus simple avant de la publier sur le site
  • Tao a indiqué que cette preuve pourrait faire l’objet d’une « vibe formalizing » dans Lean

Formalisation et vérification dans Lean

• Deux jours plus tard, Boris Alexeev a achevé la formalisation dans Lean à l’aide de l’outil Aristotle de Harmonic
  • Pour éviter les usages abusifs de l’IA, l’énoncé final a été formalisé manuellement et directement
  • L’ensemble du processus a pris environ 2 à 3 heures, et le résultat a été publié en ligne
• Tao a ensuite utilisé l’IA pour effectuer une recherche bibliographique, mais s’il a trouvé quelques travaux liés, rien n’était directement relié au problème n°367

Réactions et discussions dans la communauté

• Certains utilisateurs suivent avec intérêt, à travers les mises à jour de Tao, l’état actuel de l’usage de l’IA en mathématiques académiques
• D’autres ont exprimé une vision critique de l’approche formaliste de Lean, en soulignant que la compréhension mathématique relève de la compression, tandis que Lean la décompose en détails de bas niveau
  • Le document “Against Lean: Why Proof Assistants Formalize the Wrong Thing” affirme que Lean et les assistants de preuve similaires saisissent mal la nature profonde des mathématiques
• Un autre utilisateur a évoqué les problèmes de précision dans les conversations avec l’IA, tout en estimant que l’outil reste agréable à utiliser malgré le besoin de réglages fins

[GN⁺]

Commentaires sur Hacker News

• C’est assez bluffant de pouvoir envoyer des articles de recherche en ML très axés sur les maths à un assistant IA et récupérer une explication simple ou du pseudo-code
  Pour quelqu’un comme moi qui n’avait pas utilisé ce qu’il a appris à l’université depuis plus de 25 ans, c’est une aide énorme

  • Je me demande comment on vérifie que ces explications sont exactes. Les définitions mathématiques ont énormément de subtilités
  • Je pense justement que c’est là que les LLM excellent pour l’apprentissage
    On peut donner l’article à Claude, obtenir une vue d’ensemble, puis enchaîner avec des questions
    Même dans des domaines comme la biologie, que je n’avais pas étudiés en licence ou en master, j’ai pu creuser en profondeur comme si je discutais avec un tuteur compétent
  • La notation mathématique est très dépendante du contexte, donc si on demande à un LLM de la convertir dans un langage à faible contexte comme Lisp, on peut comprendre la structure beaucoup plus vite

• J’espère que les chercheurs et les entreprises obtiendront davantage de gains de productivité dans la recherche scientifique
  Même un assistant imparfait apporte déjà un effet de levier considérable

  • Il existe une bêta de l’application de formalisation pour iOS mentionnée par Tao → Aristotle
    Apparemment, c’est une startup fondée par le CEO de Robin Hood

• Le « vibe formalizing » ressemble à l’extension logique du « vibe engineering » et du « vibe coding »
  Quand les pièces d’un problème s’emboîtent mal, une approche de type « Move 37 as a Service », mêlant méthodes informelles et rigueur mathématique, est intéressante

  • Je m’étais déjà retrouvé bloqué en lisant un article sur la polyhedral compilation, et ChatGPT m’avait bien guidé dans le raisonnement
    Bien sûr, il y avait aussi des erreurs, mais le fait de pouvoir dialoguer en reflétant ma confusion m’a permis d’approfondir ma compréhension
    L’IA est particulièrement forte pour repérer les points de confusion chez l’utilisateur

• J’ai entendu parler de la prononciation du nom du mathématicien hongrois Erdős
  En hongrois, l’orthographe et la prononciation coïncident presque toujours, mais il y a des exceptions pour les noms
  En anglais, cela sonnerait approximativement comme « airdish »

  • Ő correspond simplement à un son œ(oe). Le -y dans les noms hongrois est une trace de la désinence -i qui indiquait autrefois une ascendance noble
    Ex. : Görgey, Széchényi, Lánczos, etc.
    L’ordre des noms hongrois suit, comme au Japon, le schéma nom de famille-prénom (big endian). Ex. : « Erdős Pál », « Neumann János »
  • J’avais vu un poème humoristique sur un panneau du département de mathématiques en 1960 — la blague disait qu’un article d’Erdos réfutait le théorème “les cercles sont ronds”
  • Comme la signification des signes de prononciation (accents de prononciation) varie selon les langues, je trouve étrange d’utiliser tels quels les signes hongrois dans une phrase anglaise
  • Au début, la prononciation « airdish » me paraissait bizarre, mais en palatalisant la terminaison « os », cela semblait assez plausible
  • N’étant pas américain, j’ai l’impression que personne ne se soucie vraiment de ce genre de questions de prononciation

• Il est intéressant de voir que certains commentaires ont une tonalité anti-Lean

  • Je ne suis pas mathématicien, mais je me demande si ce contenu anti-Lean est fiable
    J’aimerais savoir s’il s’agit simplement de promouvoir une autre approche ou d’une opposition philosophique à Lean
  • Les figures connues comme Tao attirent inévitablement beaucoup d’attention de la part des originaux et des complotistes

• Mon expérience de l’usage de l’IA en recherche mathématique est mitigée
  Elle peut parfois compléter automatiquement des raisonnements non triviaux, mais dans certains domaines elle se perd complètement
  À ce stade, je pense que l’IA est encore utile surtout comme outil d’assistance, plutôt que comme remplacement des mathématiciens

  • J’ai eu une expérience semblable. Je lui avais confié un simple problème de calcul de permutations dans un article, et cela a pris plus de temps que de le résoudre moi-même
    En programmation aussi, il lui est arrivé de ne pas repérer des bugs mineurs, mais sur des tâches complexes elle m’a beaucoup aidé
    Au final, ces outils sont encore très loin de remplacer les experts, et le surmarketing risque plutôt de nuire à la confiance
    Comme on dit, si on promet la lune, il faut la livrer ; des attentes réalistes sont essentielles

• J’ai du mal à croire que, de mon vivant, on puisse atteindre une époque façon Star Trek où l’on dira : « Ordinateur, dessine-moi la démonstration de ce problème de maths »
  J’aimerais aussi qu’on puisse dire « Beam me up Scotty »

  • Mais on risquerait de mourir à chaque fois, donc ce serait un peu problématique

• Ce soir, en conduisant, j’ai discuté avec ChatGPT de l’architecture détaillée des pipeline schedulers de LLVM et GCC
  Cela a nettement amélioré ma productivité, et il a aussi organisé automatiquement mes notes sur les expériences liées aux compilateurs
  C’était inimaginable il y a encore peu de temps

  • D’après mon expérience, il y a de fortes chances qu’un LLM se trompe sur une partie des détails
    Bien sûr, les résultats peuvent varier selon les personnes

• Si on donnait à une IA le nom Erdos, nous aurions tous un Erdos number de 1

  • Ou alors cela ferait penser à une suite de DR-DOS
  • En réalité, il existe bien un produit appelé Erdos, un IDE avec intégration IA

• J’ai été impressionné par la façon dont il a su bien exploiter les outils frontier existants pour créer un environnement de recherche mathématique collaboratif

  • Heureusement, les mathématiques restent un domaine où l’idolâtrie et les concours de popularité ne décident pas de la validité des résultats
    C’est aussi pour cela que je pense que les maths demeurent l’une des rares disciplines encore préservées de l’influence pseudo-scientifique