1 points par GN⁺ 2026-01-19 | 1 commentaires | Partager sur WhatsApp
  • Erdős #281 est un problème qui suppose une situation où, quelle que soit la manière de choisir une infinité de congruences, il ne reste presque plus d’entiers n’appartenant à aucune de ces congruences
  • La question est de savoir si, lorsque cette situation est vraie, on peut en fait dire qu’il n’est pas nécessaire d’utiliser toutes les congruences infinies et que les premières suffisent déjà à éliminer presque tous les entiers
  • Neel Somani a proposé une solution à cette question avec GPT-5.2 Pro, et plusieurs mathématiciens ont mené un examen et des compléments en se concentrant sur les étapes logiques clés
  • Au lieu de calculer directement des entiers individuels, l’approche consiste à considérer l’ensemble des entiers comme un espace unique et à traiter le problème à l’aide des propriétés de densité et de limite
  • Il est aussi apparu que la même conclusion pouvait être obtenue par combinaison de théorèmes connus antérieurement, ce qui a entraîné une discussion sur les raisons pour lesquelles ce lien était passé inaperçu si longtemps

Propositions clés de la discussion sur le problème Erdős #281

  • Erdős #281 est un problème qui suppose que, lorsqu’une infinité de congruences est donnée, presque tous les entiers finissent par appartenir à l’une d’elles, quelle que soit la manière de choisir ces congruences
  • Le cadre suppose qu’on sait déjà que, si l’on applique toutes les congruences, il ne reste presque plus d’entiers n’appartenant à aucune d’entre elles
  • La question posée est de savoir si, lorsque cette propriété est vérifiée, un effet presque identique apparaît déjà à une étape finie, sans devoir utiliser jusqu’au bout l’infinité de congruences
  • La structure du problème demande si un résultat valable à l’étape infinie est automatiquement garanti aussi à une étape finie
  • Il subsiste une difficulté pour affirmer qu’un nombre fini de congruences suffit, dans des conditions où l’on autorise toujours le pire choix possible de classes résiduelles

L’approche de la solution de Neel Somani et GPT-5.2 Pro

  • Une approche qui, au lieu d’examiner les entiers un par un, considère l’ensemble des entiers comme un espace unique et traite le problème via la notion de densité
  • Une manière de procéder qui consiste à définir comme objet l’ensemble des entiers évitant les k premières congruences
  • Exploitation de la structure selon laquelle cet ensemble se réduit à mesure que k grandit et converge vers le résultat à l’étape infinie
  • Déroulement logique selon lequel, à partir de l’hypothèse qu’il existe très peu d’entiers évitant toutes les congruences infinies, l’ensemble doit nécessairement devenir suffisamment petit dès une étape finie
  • Construction du raisonnement général à l’aide des limites, des moyennes et des propriétés de translation

Le processus de vérification et l’évolution de la discussion

  • Examen attentif, dans la solution proposée, de la légitimité de l’ordre dans lequel on prend les limites et de la manière de traiter les moyennes
  • Apparition de remarques indiquant que certaines étapes nécessitaient des explications supplémentaires et des compléments
  • Processus au cours duquel plusieurs mathématiciens ont vérifié publiquement le raisonnement et clarifié le sens de chaque étape
  • Au final, une argumentation dont la structure essentielle a été conservée tout en étant affinée sous une forme plus claire

Le lien avec des théorèmes classiques

  • Confirmation que la même conclusion peut aussi être obtenue en combinant des théorèmes connus de longue date
  • Combinaison d’un résultat traitant de la convergence de densité sous une infinité de conditions et d’un théorème expliquant le pire cas sous des conditions finies
  • Cette connexion révèle une structure où les propriétés de l’étape infinie se reflètent fortement aussi à l’étape finie
  • Diffusion d’une discussion sur les raisons pour lesquelles ce lien n’avait pas été clairement formulé pendant si longtemps

Pourquoi ce cas attire l’attention

  • Un cas où un problème posé de longue date a été remis au centre de l’attention à la faveur d’une proposition de solution fondée sur l’IA
  • Plutôt qu’un cas où l’IA aurait seule fourni une réponse achevée, il s’agit d’un déclencheur de discussion à partir d’un point de vue nouveau
  • Confirmation que la difficulté peut varier fortement selon le langage et le cadre conceptuel dans lesquels on reformule le problème

1 commentaires

 
GN⁺ 2026-01-19
Réactions sur Hacker News
  • On disait auparavant qu’il n’existait pas de solution, mais on a désormais retrouvé une solution préexistante
    La preuve générée par le LLM a donc été déplacée vers la section 2 du wiki de Terence Tao
    La discussion associée se trouve dans ce post du forum erdosproblems
    • La remarque de Tao est intéressante — il dit que la nouvelle preuve est assez différente de celle de la littérature existante
      Plus étrange encore, cette preuve figurait dans un article de Erdős lui-même, alors qu’il avait tout de même laissé le problème comme non résolu
    • On dirait que ces modèles fonctionnent comme des moteurs de recherche en langage naturel qui relient des points de connaissance que les humains n’avaient pas connectés
    • En réalité, ce cas montre que le problème en lui-même n’a pas grande importance
      S’il existait déjà une solution sans que personne ne le sache, c’est parce que les gens ne s’y intéressaient pas
      Fouiller simplement l’ancienne littérature et appeler cela un « nouveau progrès » peut relever d’un progrès illusoire
      Une grande partie des mathématiques pures finit par donner l’impression d’un simple jeu de puzzle intellectuel
  • Je me demandais quelle était la nature des problèmes d’Erdos — des casse-têtes sur lesquels les mathématiciens ont lutté pendant des années, ou bien des problèmes délaissés
    D’après l’explication sur le wiki de Tao,
    les problèmes d’Erdos ont des niveaux de difficulté très variés, et certains sont classés parmi les problèmes de faible difficulté bien adaptés à l’IA
    • Erdos était un mathématicien extrêmement prolifique, qui aimait proposer des problèmes avec récompense
      Les problèmes faciles étaient d’un niveau tel que « même les meilleurs mathématiciens ne les résolvaient pas immédiatement », ce qui en fait un bon indicateur des performances de l’IA
      À mesure que l’IA progresse, elle gravira l’échelle de difficulté vers des problèmes de plus en plus ardus
    • Pas besoin de trop s’inquiéter. Ni Tao ni l’auteur ne s’intéressaient beaucoup aux problèmes d’Erdos,
      et aucun des deux ne savait que la preuve figurait dans un article d’Erdos lui-même
      Pourtant, le Fediverse et Twitter en parlent comme d’une percée des LLM
  • D’après un commentaire laissé directement par Tao sur le forum,
    il a été impressionné par le fait que le LLM ait évité les erreurs d’échange de limites ou de manipulation des quantificateurs
    Il a ajouté qu’un modèle de génération précédente se serait probablement trompé sur ce genre de points,
    et a précisé qu’il avait inscrit ce résultat dans la section 1 du wiki
    • Ensuite, quelqu’un a fouillé davantage la littérature et a découvert que le même résultat avait déjà été démontré dans un article de Davenport et Erdos en 1936
      Tao a commenté : « la nouvelle preuve est différente de l’existante, mais je la déplace en section 2 »
  • J’aimerais bien que l’IA commence par prouver ses propres affirmations
    Les modèles récents disent avec assurance produire du « code parfait à 100 % », mais en pratique ça plante
    Même en essayant de payer z.ai, une erreur s’est produite et l’achat n’a même pas abouti
    Les LLM sont une technologie impressionnante, mais en même temps surévaluée
    • Pour vérifier le code d’une IA, il faut le démontrer comme on le ferait pour un humain, avec des tests ou des preuves
      Il faut des éléments empiriques comme des logs ou des résultats d’exécution
    • Il faut distinguer le modèle et l’app
      Le modèle ne fait que générer du texte, et c’est à l’app de le vérifier
      Mais une génération de texte parfaite est actuellement impossible
  • Il existe un fil du forum erdosproblems auquel Tao a participé directement
  • Je me demandais si cette preuve avait vraiment été vérifiée
    parce que j’ai souvent vu des LLM produire avec aplomb des réponses fausses
    La politique de mémoire et les restrictions d’accès aux modèles chez OpenAI sont aussi un sujet intéressant
    • Tao l’a approuvée lui-même. Difficile d’imaginer validation plus solide
  • Il y a eu récemment un post affirmant que l’Aristotle de Harmonic avait résolu le problème Erdős 728
    Ici, on parle d’un cas où ChatGPT 5.2 a donné une réponse en une heure,
    mais on ne sait pas clairement si c’est reproductible, pourquoi il a proposé cette solution, ni ce qu’il a effectivement démontré
    La validation de Tao inspire confiance, mais au fond la question reste : « le modèle a-t-il été entraîné pour mieux convenir aux mathématiques pures ? »
    Voir le cas précédent et le lien vers la session ChatGPT
    • Il y a 49 jours déjà, il y avait eu un cas où le problème #124 avait été démontré par une IA
      Lien associé
    • Cela s’inscrit dans une série de tentatives où des LLM génèrent des preuves candidates pour des problèmes mathématiques,
      puis celles-ci sont vérifiées avec des systèmes de preuve formelle comme Lean
      Tao examine d’abord la justesse de la preuve, puis vérifie son originalité par recherche bibliographique
      Pour l’instant, il y a très peu de preuves entièrement nouvelles, mais de nouvelles approches commencent à apparaître
      Dans ce cas aussi, cela ressemblait d’abord à une nouvelle preuve, avant qu’on découvre que c’était finalement un résultat qu’Erdos connaissait déjà
  • J’ai donné le même prompt à Deepseek, qui l’a résolu bien plus vite que ChatGPT
    Puis j’ai soumis les deux preuves à Opus, qui a dit qu’elles étaient équivalentes
    • Mais certains font remarquer que « c’est à peu près comme si tu t’étais toi-même mis un tampon d’approbation »,
      et que si la vérification détaillée manque, toute la preuve peut s’effondrer
    • Sur le plan mathématique, certains doutent que la partie sur la densité de l’intersection soit suffisante
      Le contre-exemple potentiel évoqué prend les ensembles (U_k)
    • Le bloc de raisonnement de Kimi-k2 a aussi été partagé
    • Certains se demandent aussi si Deepseek n’a pas simplement mémorisé la solution existante
      Voir cette discussion dans ce commentaire
    • D’autres estiment qu’Opus ne convient pas aux maths
      Sa précision mathématique est inférieure à celle de ChatGPT ou Gemini Pro
  • Il est frappant de constater qu’une part importante des preuves produites par LLM vient de non-spécialistes
    D’où la question : certains mathématiciens professionnels utilisent-ils l’IA sans le dire ?
    • En réalité, la plupart des spécialistes semblent penser que « dans mon domaine, les LLM sont idiots »
    • Cet usage anonyme de l’IA va sans doute se généraliser
      Un peu comme une course au dopage dans le sport, où tout le monde s’y met pour ne pas être distancé
      En plus, utiliser l’IA n’enfreint aucune règle
    • En pratique, il est très probable que les experts aient déjà essayé,
      mais que les LLM n’aient pas encore produit de progrès substantiels
    • On réfléchit à la manière de signaler les contributions de l’IA
      Personnellement, je pense qu’une ligne de remerciements est appropriée
      En tant que postdoc en maths, j’ai testé GPT 5.2 et je l’ai trouvé moins menteur et plus honnête en cas d’échec
      À l’inverse, Gemini 3 a tendance à inventer des théorèmes lorsqu’il se trompe
  • Je me demande si les problèmes d’Erdos résolus par des LLM sont simplement des problèmes faciles laissés de côté par les humains,
    ou s’il s’agit de vraies contributions de recherche originales
    • D’après l’avertissement sur le wiki de Tao,
      les problèmes d’Erdos présentent une forte dispersion de difficulté, et il existe un groupe de problèmes de faible difficulté faciles à résoudre pour l’IA
    • Malgré tout, il est utile que les LLM fassent le tri dans ces problèmes de faible difficulté
      Si un problème figure sur la liste d’Erdos, il est probable qu’au moins quelqu’un ait essayé de le résoudre au moins une fois