▲

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

 (twitter.com/BoWang87)
2P by GN⁺ 20시간전 | ★ favorite | 댓글 1개
  • 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/)에 공개됨
▲
GN⁺ 20시간전  [-]
Hacker News 의견들

  • 나는 늘 AI가 맥도날드를 운영하기 전에 필즈상을 받을 것이라 말해왔음
    수학은 인간에게 망치로 나사를 돌리는 일처럼 어렵게 느껴짐
    LLM은 얕지만 넓은 탐색에 강해서 새로운 수학적 패턴을 많이 발견하고 있음
    앞으로는 LLM 대신 Lean 구문 트리 기반의 AlphaGo식 강화학습으로 전환될 거라 예측함
    수학자들이 쓰는 ‘10가지 트릭’을 잠재 벡터로 코딩할 수 있다면 게임 끝임

    • 트릭은 결국 논리식의 패턴일 뿐임
      우리는 기하학적 유추를 통해 대수기하를 수론 문제에 적용하듯 사고함
      Lean 트리로 학습된 AI는 인간보다 더 넓은 직관 체계를 가질 수도 있음
      체스에서 StockFish가 보여준 사례처럼, 이런 접근을 기계적 해석 가능성(mechanistic interpretability) 관점에서 연구해볼 가치가 있음
    • 나는 전문 수학자인데, 좋은 증명은 문제의 표현 방식이 핵심임
      트릭을 꺼내 쓰는 건 LLM도 이미 잘함
      하지만 문제를 올바르게 표현하는 부분은 여전히 인간의 몫이며, 그게 자연스러움
    • 만약 시스템이 스스로 새로운 트릭을 발견하도록 학습된다면 정말 놀라운 일일 것임
    • “AI가 맥도날드를 운영하기 전에 필즈상을 받을 것”이라는 말이 너무 마음에 듦
      나는 여기에 “마지막으로 자동화될 직업은 QA”라는 내 버전을 덧붙이고 싶음
      이번 기술 물결은 지식 노동의 본질을 다시 생각하게 만들었고, 그 덕에 우리는 더 날카로워질 것임
    • 나도 Lean 트리 기반 강화학습 접근을 직접 프로토타입으로 구현해보려 천천히 시도 중임

  • 예전에 “trolls trolling trolls”라는 4chan 격언을 배우고 나서부터 인터넷 상호작용을 항상 의심의 눈으로 보게 되었음
    Reddit이 이미 ‘죽은 인터넷’이 되었다고 느꼈는데, 이번 스레드를 보니 이제는 누가 봇인지 인간인지 구분이 안 됨

    • 그 통찰이 정말 중요하다고 생각함
      그래서 나는 RememberBuddy라는 서비스를 만들었음 — 일상 속 통찰을 잊지 않게 저장하는 공간임

  • AI 수학의 진화는 90년대 Greg Egan이 소설에서 예견한 궤적을 따를 것 같음
    수학의 본질은 변하지 않지만, ‘왜’ 하는지는 달라질 것임
    Egan의 『Diaspora』에서는 수학적 발견이 마치 소금광산에서 보석을 캐는 행위처럼 묘사됨
    어떤 이는 그 보석 자체의 순수한 아름다움을, 또 어떤 이는 실용적 가치를 추구함
    현재 Terence Tao가 세운 연구소 같은 곳이 이런 미래와 맞닿아 있음
    단기적으로는 이런 연구가 AI 시스템의 정확한 정보 생성 능력을 크게 향상시킬 것임

  • 어떤 사람들은 지식 발견이 단순히 과거 행동을 흉내 내는 것이라고 생각하지만, 나는 그렇지 않다고 봄

  • 전문가가 모델을 잘 이끌면 대부분의 문제는 해결 가능함
    모델은 전문가의 게으른 작업을 대신하는 도구로는 훌륭하지만, 복잡한 문제에서는 여전히 맹점이 존재함

  • 논문에서 시스템 프롬프트 일부를 봤는데,
    “모든 exploreXX.py 실행 후 즉시 plan.md를 업데이트하라”는 규칙이 있었음
    이런 프롬프트가 고급 문제 해결 성능을 향상시키는 이유가 궁금함

    • 아마도 과정을 잃지 않고 재시작하기 쉽게 만들기 위한 장치일 것임

  • 우리는 점점 “구독형 지능(intelligence as a subscription)” 이라는 OpenAI CEO의 비전에 가까워지고 있음

  • 탭 전환을 줄이는 게 과소평가되고 있음
    AI 도구의 절반은 UX 문제가 아니라 모델 접근의 안정성 확보 싸움임

  • “100마리 원숭이에게 100자루 총과 건축 자재를 주면 집을 지을까, 아니면 은행을 털까?”
    그 결과가 나온다면 그것이 의도된 행동인지 묻고 싶음

  • 이 트윗을 봤는데

    • 댓글 대부분이 명백히 AI가 생성한 문장 패턴처럼 보였음 — “그건 X가 아니라 Y야” 식의 반복임
답변달기