Knuth의 ‘Claude Cycles’ 문제에서 인간·AI·증명 보조기의 협업 진전

• Donald Knuth가 제시한 Hamiltonian 분해 문제의 미해결 부분이 인간과 AI의 협업으로 확장 해결됨
• Claude가 홀수 m의 해법을 찾아 “Claude’s Cycles” 로 명명되었으며, 이후 11,502개 순환 중 996개가 모든 홀수 m에 일반화됨
• Dr. Ho Boon Suan이 GPT-5.4 Pro로 짝수 m≥8에 대한 14쪽 증명과 m=2000까지 계산 검증을 수행
• Dr. Keston Aquino-Michaels는 GPT와 Claude의 다중 에이전트 워크플로로 홀수·짝수 m 모두에 대한 단순한 구성법을 발견
• Dr. Kim Morrison이 Lean 증명 보조기로 Knuth의 해법을 형식 검증하며, 인간·AI·증명 도구의 협업 생태계가 완성됨

Claude의 Cycles 문제 해결의 확장된 협업

• Donald Knuth가 제시한 Hamiltonian 분해 문제의 미해결 부분이 인간과 AI의 협업으로 해결됨
  • 초기에는 Claude가 약 한 시간의 탐색으로 홀수 m에 대한 해법을 찾아 Knuth가 이를 “Claude’s Cycles” 로 명명
• 이후 업데이트된 논문에서 기초 사례 m=3의 경우 정확히 11,502개의 Hamiltonian 순환이 존재하며, 그중 996개가 모든 홀수 m으로 일반화됨
  • Knuth는 이 중 760개의 유효한 “Claude형” 분해를 확인
• 짝수 m의 경우 Claude가 완성하지 못했으나, Dr. Ho Boon Suan이 GPT-5.4 Pro를 이용해 m≥8에 대한 14쪽짜리 증명을 작성하고 m=2000까지 계산 검증을 수행
• 이어서 Dr. Keston Aquino-Michaels가 GPT와 Claude를 함께 사용하는 다중 에이전트 워크플로를 통해 홀수·짝수 m 모두에 적용 가능한 단순한 구성법을 발견
• Dr. Kim Morrison은 Knuth의 홀수 해법을 Lean 증명 보조기에서 형식화하여 검증
  • 결과적으로 인간, 여러 AI 시스템, 그리고 형식 증명 도구가 병렬로 협력하는 완전한 수학적 협업 생태계가 형성됨
• 이 일련의 과정은 한 AI의 단일 문제 해결에서 출발해, 다중 AI·인간·증명 보조기 협업으로 확장된 새로운 수학 연구 모델을 보여줌
• 최신 논문은 Stanford CS Faculty 웹사이트(www-cs-faculty.stanford.edu/~knuth/papers/)에 공개됨