- La partie non résolue du problème de décomposition hamiltonienne proposé par Donald Knuth a été résolue de manière étendue grâce à la collaboration entre humains et IA
- Claude a trouvé une solution pour les m impairs, baptisée ensuite « Claude’s Cycles », puis 996 des 11 502 cycles ont été généralisés à tous les m impairs
- Dr Ho Boon Suan a produit, avec GPT-5.4 Pro, une preuve de 14 pages pour les m pairs ≥8 et une vérification computationnelle jusqu’à m=2000
- Dr Keston Aquino-Michaels a découvert une méthode de construction simple pour les m impairs et pairs grâce à un workflow multi-agents avec GPT et Claude
- Dr Kim Morrison a formellement vérifié la solution de Knuth avec l’assistant de preuve Lean, complétant ainsi un écosystème collaboratif entre humains, IA et outils de preuve
Extension de la collaboration pour résoudre le problème des Claude’s Cycles
- La partie non résolue du problème de décomposition hamiltonienne proposé par Donald Knuth a été résolue grâce à la collaboration entre humains et IA
- Au départ, Claude a trouvé en environ une heure d’exploration une solution pour les m impairs, que Knuth a baptisée « Claude’s Cycles »
- Dans une version mise à jour de l’article, pour le cas de base m=3, il existe exactement 11 502 cycles hamiltoniens, dont 996 se généralisent à tous les m impairs
- Knuth a confirmé parmi eux 760 décompositions valides de type « Claude »
- Pour les m pairs, Claude n’avait pas pu aller jusqu’au bout, mais Dr Ho Boon Suan a utilisé GPT-5.4 Pro pour rédiger une preuve de 14 pages pour m≥8 et effectuer une vérification computationnelle jusqu’à m=2000
- Ensuite, Dr Keston Aquino-Michaels a découvert, via un workflow multi-agents utilisant GPT et Claude ensemble, une méthode de construction simple applicable à la fois aux m impairs et aux m pairs
- Dr Kim Morrison a formalisé et vérifié dans l’assistant de preuve Lean la solution de Knuth pour le cas impair
- Au final, un écosystème mathématique collaboratif complet s’est mis en place, où humains, plusieurs systèmes d’IA et outils de preuve formelle coopèrent en parallèle
- Cette série d’étapes montre comment la résolution d’un problème par une seule IA a évolué vers un nouveau modèle de recherche mathématique fondé sur la collaboration entre plusieurs IA, des humains et des assistants de preuve
- Le dernier article est publié sur le site Stanford CS Faculty(www-cs-faculty.stanford.edu/~knuth/papers/)
1 commentaires
Commentaires sur Hacker News
J’ai toujours dit que l’IA remportera une médaille Fields avant de gérer un McDonald’s
Les maths semblent difficiles pour les humains, comme visser une vis avec un marteau
Les LLM excellent dans l’exploration large mais superficielle, et découvrent déjà beaucoup de nouveaux motifs mathématiques
Je prédis qu’on passera ensuite des LLM à un apprentissage par renforcement façon AlphaGo basé sur des arbres syntaxiques Lean
Si on peut encoder les « 10 trucs » des mathématiciens sous forme de vecteurs latents, la partie est finie
Nous raisonnons en appliquant des analogies géométriques à des problèmes de théorie des nombres, comme lorsqu’on applique la géométrie algébrique
Une IA entraînée sur des arbres Lean pourrait avoir un système d’intuition plus large que celui des humains
Comme l’a montré StockFish aux échecs, cette approche vaudrait la peine d’être étudiée du point de vue de l’interprétabilité mécaniste (mechanistic interpretability)
Sortir un truc au bon moment, les LLM savent déjà bien le faire
Mais la partie qui consiste à représenter correctement le problème reste encore du ressort des humains, et c’est naturel
J’ai envie d’y ajouter ma propre version : le dernier métier à être automatisé sera la QA
Cette vague technologique nous pousse à repenser la nature du travail intellectuel, et cela va nous rendre plus affûtés
Depuis que j’ai appris l’adage de 4chan « trolls trolling trolls », je regarde toujours les interactions sur Internet avec suspicion
J’avais déjà l’impression que Reddit était devenu un « internet mort », et en voyant ce fil, je n’arrive plus à distinguer qui est un bot et qui est humain
C’est pour ça que j’ai créé RememberBuddy — un espace pour conserver les intuitions du quotidien et éviter de les oublier
L’évolution de l’IA en mathématiques semble suivre la trajectoire que Greg Egan avait anticipée dans les années 1990 dans ses romans
La nature des mathématiques ne changera pas, mais la raison pour laquelle on en fait changera
Dans Diaspora d’Egan, la découverte mathématique est décrite comme le fait de dégager des gemmes dans une mine de sel
Certains recherchent la beauté pure de ces gemmes, d’autres leur valeur pratique
Des lieux comme l’institut fondé aujourd’hui par Terence Tao touchent déjà à cet avenir
À court terme, ce type de recherche améliorera fortement la capacité des systèmes d’IA à produire des informations exactes
Certaines personnes pensent que la découverte de connaissances consiste simplement à imiter des comportements passés, mais je ne suis pas d’accord
Quand un expert guide bien le modèle, la plupart des problèmes peuvent être résolus
Le modèle est excellent comme outil pour prendre en charge le travail pénible de l’expert, mais sur les problèmes complexes, il existe encore des angles morts
J’ai vu une partie du system prompt dans l’article,
il y avait une règle disant : « après chaque exécution de exploreXX.py, mets immédiatement à jour plan.md »
Je me demande pourquoi ce genre de prompt améliore les performances sur des problèmes avancés
Nous nous rapprochons de plus en plus de la vision du CEO d’OpenAI d’une « intelligence sur abonnement (intelligence as a subscription) »
La réduction des changements d’onglet est sous-estimée
La moitié des outils IA relèvent moins d’un problème d’UX que d’une bataille pour sécuriser un accès stable au modèle
« Si on donne à 100 singes 100 fusils et des matériaux de construction, vont-ils construire une maison ou braquer une banque ? »
Si un tel résultat se produisait, je voudrais demander si c’était un comportement intentionnel
J’ai vu ce tweet