A First Proof Sprint

논문 개요

이 논문은 2026 년 2 월 11 일부터 13 일까지 약 55 시간 동안 진행된 **'첫 번째 증명 스프린트 (First Proof Sprint)'**의 결과와 방법론을 보고합니다. 인간 디스패처와 여러 AI 에이전트 (Claude, Codex) 가 협력하여 10 개의 연구 수준 (research-level) 수학 문제를 해결하려는 시도를 기록한 것으로, 생성된 초안과 적대적 검증 (adversarial verification), 표적 수정, 명시적 출처 추적 (provenance) 을 결합한 다중 에이전트 워크플로우를 제시합니다.

1. 문제 정의 및 배경

• 목표: 10 개의 다양한 수학 분야 (확률적 편미분방정식, 자동형식, 대수적 위상수학, 그래프 이론, 기하학 등) 의 열린 문제를 해결하거나 부분적으로 해결하는 것.
• 문제 유형:
  • P1: $\Phi^4_3$ 측도의 매끄러운 이동 하에서의 측도 동치성.
  • P2: Rankin-Selberg 적분을 위한 보편적 테스트 벡터 존재 여부.
  • P3: ASEP 다항식 정상 분포를 갖는 마코프 체인 구성.
  • P4: 유한 자유 합성 (finite free convolution) 하에서의 근 분리 에너지 부등식 ($n=4$ 경우).
  • P5: $O$-슬라이스 연결성과 기하학적 고정점.
  • P6: 그래프의 $\epsilon$-가벼운 정점 부분집합 존재성.
  • P7: 2-토션 (2-torsion) 을 포함하고 유리수 계수 아시클릭 (acyclic) 보편 피복을 갖는 균일 격자.
  • P8: 4-가 (4-valent) 정점을 가진 다면체 표면의 라그랑지안 매끄러움 (smoothing).
  • P9: 4 초점 텐서 (quadrifocal tensors) 에 대한 랭크 -1 스케일링의 다항식 탐지.
  • P10: RKHS 제약 조건 하의 텐서 CP 분해에 대한 PCG (Preconditioned Conjugate Gradient) 방법.

2. 방법론 (Methodology)

이 프로젝트의 핵심은 Lakatos 의 "증명과 반증 (Proofs and Refutations)" 모델을 AI 속도로 구현한 것입니다.

• 다중 에이전트 협업:
  • 생성자 (Provers): Claude Max 를 사용하여 초기 증명 초안 생성.
  • 비평가 (Critic): Codex 를 사용하여 주장의 과장 (overclaims) 과 숨겨진 간극을 적대적으로 검증.
  • 디스패처 (Human Dispatcher): 인간 연구자가 흐름을 조정하고 수정 방향을 제시.
• 와이어링 다이어그램 (Wiring-Diagram) 분해:
  • 각 증명을 **선언과 의존성의 유형화된 그래프 (typed graph of claims and dependencies)**로 표현.
  • 이 구조적 그래프는 논리적 결함을 전체 문서 수준이 아닌 국소적 (local) 으로 격리하고, 검증자 (verifier) 가 특정 노드만 재검토하도록 하여 효율성을 극대화했습니다.
• 반복적 검증 및 수정:
  • 초기 "모두 해결됨"이라는 태도에서 시작하여, 검증 과정에서 발견된 간극을 기반으로 결과를 **완결 (Closed), 부분적 (Partial), 조건부 (Conditional)**로 명확히 분류하는 과정으로 전환되었습니다.
• 계산적 스트레스 테스트:
  • 수치적 검증 (Python, SymPy, PHCpack 등) 을 통해 추측된 분기를 제한하고, 특히 $n=4$와 같은 고차원 문제에서 대수적 증명의 타당성을 확인했습니다.

3. 주요 결과 (Key Results)

10 개 문제의 최종 상태는 다음과 같이 분류되었습니다 (기호: [수학적 상태 | 검증 상태]):

• 완결됨 (Mathematically Closed & Validated):
  • P1, P2, P3, P8: 수학적으로 증명되었으며 검증이 완료됨. (P2 는 인용된 새로운 벡터 정리에 의존).
  • P5: 국소적 범위 (FO-local connective spectra) 내에서 해결됨.
• 부분적 (Partial):
  • P4: $n \le 3$은 분석적으로 증명, $n=4$는 Path 2 대수적 인증서로 증명됨. $n \ge 5$는 미해결.
  • P6: 완전 그래프 ($K_n$) 경우 $c_0 = 1/3$으로 증명됨. 일반 그래프는 특정 기술적 간극 (Barrier Maintenance Invariant) 이 남아 조건부.
  • P9: 강력한 계산적 증거가 있으나, 보편적 역방향 (universal converse) 단계의 대수적 폐쇄가 미완성.
• 조건부 (Conditional):
  • P7: 회전 경로 (rotation route) 를 통해 수학적으로 잠정 해결됨. 독립적인 장부 (ledger) 재검증이 필요.
  • P10: 명시된 가정 하에 조건부 해결됨.

4. 주요 기여 (Key Contributions)

1. 구조 인식 검증 (Structure-Aware Verification):
   • 단순한 내러티브 작성보다 와이어링 다이어그램 기반 검증이 논리적 간극과 불일치를 더 효과적으로 식별하고 국소화함을 입증했습니다.
2. 레이어 스위칭 전략 (Layer-Switching Strategies):
   • 특정 문제 (예: P6, P7) 에서 고전적 접근이 막히면 다른 수학적 층위 (예: 대수적에서 기하학적, 또는 반대로) 로 전환하여 해결책을 찾는 전략의 유효성을 보여줌.
3. 명시적 결과 분류 체계:
   • AI 가 생성한 증명의 신뢰도를 높이기 위해 "완결", "부분적", "조건부"를 명확히 구분하고, 미해결 과제를 명시적인 다음 단계 (named, testable next steps) 로 기록하는 프로세스를 정립했습니다.
4. 적대적 피드백 루프:
   • 생성 - 비판 - 수정의 반복이 초기의 과장된 주장을 제거하고 실제 증명 가능한 결과로 수렴하게 만드는 핵심 동력임을 입증.

5. 의의 및 시사점

• 수학적 발견의 자동화: 이 프로젝트는 컴퓨터가 추측, 비판, 재구성을 통해 수학적 발견 과정에 참여할 수 있음을 보여주는 실증적 사례입니다.
• 신뢰성 있는 AI 수학: 생성 속도는 빠르지만 신뢰할 수 있는 검증은 느리다는 비대칭성을 인정하고, 이를 구조화된 검증 도구 (노드 단위 검증, 의존성 그래프) 로 보완하는 방법론을 제시했습니다.
• 실시간 논증 구조: Lakatos 의 대화 모델을 기계 속도로 구현하여, 복잡한 연구 문제에서도 체계적인 논증 구조를 유지하며 협업할 수 있음을 보였습니다.
• 미래 방향: 이 작업은 "실시간 논증 구조 (Real-Time Argumentation Structure)"와 "교차 문제 학습 (Cross-Problem Learning)"을 위한 토대를 마련하며, AI 와 인간이 협력하여 연구 수준 문제를 해결하는 새로운 패러다임을 제시합니다.

결론

"A First Proof Sprint"는 AI 에이전트들이 인간 연구자의 감독 하에 10 개의 난제를 처리한 성공적인 실험입니다. 핵심 성과는 10 개의 문제를 모두 완벽하게 해결한 것이 아니라, 구조화된 검증 도구와 적대적 피드백 루프를 통해 증명 과정의 신뢰성을 높이고, 미해결 부분을 명확히 식별하여 연구의 지평을 넓혔다는 점에 있습니다. 이는 향후 대규모 수학 문제 해결을 위한 AI-인간 협업 시스템의 중요한 마일스톤이 됩니다.