Tu codes avec l’IA ?
Outils, agents et nouveautés dev IA décryptés, chaque soir en 5 min. Gratuit.
Inclus dès l'inscription : notre sélection des meilleurs guides & comparatifs IA.
Choisis ton rythme
Gratuit · Pas de spam · Désabonnement en 1 clic
OpenAI publie 372 résultats mathématiques produits par un modèle interne et les place sur GitHub avec des éléments de vérification automatique. Tandis que l’entreprise promet davantage de formalisations et détaille sa méthodologie, des mathématiciens de premier plan alertent sur les limites d’une production à grande échelle et sur ses effets sur la discipline.
Des mises en garde de médaillés Fields et des limites de Lean
Les formalisation en Lean permettent de certifier la cohérence logique d'une preuve, mais ne tranchent ni sa pertinence ni son originalité. Vingt-cinq lauréats de la médaille Fields ont signé une lettre ouverte signalant un décalage profond entre les objectifs de l'industrie de l'IA et ceux des mathématiques. Ils y soutiennent que la résolution de problèmes n'est qu'un moyen, loin de l'objectif de compréhension conceptuelle, et que la production de masse d'énoncés vrais risquerait d'appauvrir le terrain d'idées. Timothy Gowers prévient qu'à l'horizon d'une à deux décennies, la littérature pourrait enfler sans qu'une communauté humaine ne la comprenne réellement. Terence Tao plaide pour une formation des jeunes axée sur l'humain et une limitation stricte des outils d'IA afin de préserver un apprentissage authentique. Les réactions évoquées vont de l'enthousiasme à l'irritation, tandis qu'OpenAI mise de son côté sur des avancées aux frontières de la connaissance.
372 résultats publiés sur GitHub avec vérifications Lean
OpenAI diffuse 372 résultats mathématiques issus d'un modèle interne et choisit GitHub comme vecteur plutôt que des revues. Une part importante des preuves s'accompagne de formalisations en Lean, et d'autres sont annoncées. La collection rassemble des améliorations d'algorithmes majeurs et des avancées autour de l'hypothèse de Riemann. Les documents sont fournis avec journaux de révision et citations, et chaque résultat est présenté comme résolvant un problème ouvert ou apportant des progrès substantiels. L'entreprise décrit le modèle générateur comme un système de pointe.
Production : un agent par requête et trois heures de calcul en moyenne
OpenAI indique que la plupart des résultats proviennent d'une seule requête à un seul agent, avec parfois plusieurs tentatives. En moyenne, chaque résultat requiert environ trois heures de calcul avec ChatGPT Pro. À l'inverse, une solution à un problème de Navier-Stokes, attribuée au même modèle, a mobilisé un essaim de 10 000 agents et des millions de dollars de calcul et fait l'objet d'une révision formelle depuis plusieurs semaines. L'entreprise publie des résumés de raisonnement, des statistiques sur les problèmes tentés et des estimations de coûts, et avance que l'ampleur de la production pourrait dépasser les capacités de relecture manuelle, ce qui motive l'usage de la vérification formelle.
Processus et gouvernance : IAS consulté et ateliers annoncés
OpenAI déclare avoir sollicité le Groupe consultatif sur les mathématiques et l'IA de l'Institut d'études avancées, où siège notamment Timothy Gowers, et dit avoir suivi de façon lâche ses recommandations publiques en ne publiant pas les requêtes et en ne communiquant que des coûts moyens. L'entreprise prévoit de financer des ateliers et conférences dédiés à l'appropriation de ces résultats, souhaite rehausser la qualité des citations et de la présentation, et travaille à une publication responsable du modèle. Le choix de GitHub plutôt que de revues à comité de lecture structure la diffusion de ce corpus.
