Progrès de la collaboration entre humains, IA et assistant de preuve sur le problème des « Claude Cycles » de Knuth

• 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/)