Conway의 정제 추측 증명을 '바이브'로 풀어낸 방법

핵심 요약

Dan Abramov는 Claude, ChatGPT, Codex 에이전트를 사용하여 전능 정수(omnific integers)에 대한 Conway의 정제 추측 증명을 생성, 검토 및 Lean 형식화했습니다. 이 증명은 기계적 검증은 통과했으나 아직 독립적인 검증은 이루어지지 않았습니다.

Conway의 추측이란 무엇인가

Conway의 정제 추측은 *전능 정수(omnific integers)*의 곱에 대한 모든 등식 (a b = c d)에 대하여 다음을 만족하는 정수 (e,f,g,h)가 존재한다고 주장합니다:

(a = e f)
(b = g h)
(c = e g)
(d = f h)

즉, 전능 정수의 임의의 두 인수분해는 공통된 정제를 가지며, 이는 곱을 소인수로 분해하고 재조합할 수 있다는 초등 정수의 성질을 반영합니다.

AI 기반 연구 파이프라인

1. 문제 선정

Claude에게 초현실 수(surreal numbers) 분야의 미해결 문제를 선택하도록 요청했습니다. Claude는 L’Innocente와 Mantova의 최근 연구를 인용하며 이 추측을 (K((\mathbb{R}^{\le 0}))) 내의 기약원(irreducibles)에 관한 진술로 축소한 정제 추측을 선택했습니다.
저자는 Claude의 축소 과정이 불완전했음을 지적했지만, ONAG 50주년이라는 상징적 의미 때문에 이 문제를 계속 진행하기로 했습니다.

2. 초기 원샷 시도

초기 프롬프트에서는 Claude에게 "획기적인 성과를 내라"고 요청했습니다. 모델은 검증 불가능한, 전문 용어로 가득 찬 일관성 없는 글을 생성했습니다.
ChatGPT(이하 Sol)로 전환하자 더 겸손한 주장이 나왔지만, 여전히 광범위한 인간의 검토가 필요했습니다.

3. 다중 에이전트 연구소 (Codex)

프로젝트 관리자(PM) 에이전트가 워크플로우를 조정했습니다.
두 명의 수학(Math) 에이전트가 후보 보조 정리를 생성했습니다.
레드(Red) 에이전트가 결함을 찾으려 시도했습니다.
랜덤(Random) 에이전트가 주변 아이디어를 탐색했습니다.
Lean 에이전트가 유망한 결과를 Lean 코드로 번역했습니다.
에이전트들은 "카페테리아" 채팅방을 통해 소통하며 역할 경계를 유지하면서도 아이디어를 교류했습니다.

4. 토큰 소비 및 비용

약 400억 토큰이 처리되었으며, 그중 약 2억 1천만 토큰이 출력되었습니다.
예상 API 비용: ≈ 40,000달러.

주요 이정표

주차	이정표	결과
1	문제 설정 및 초기 프롬프트	Claude는 모호한 문제 진술을 생성; ChatGPT는 비판적인 "회의적" 목소리를 제공.
2	Codex 에이전트를 이용한 연구소 설정	수십 개의 초안 "논문" 생성; 다수가 발명된 용어와 논리적 공백을 포함함.
3	첫 번째 막다른 길 및 실패한 "부트스트랩" 증명	ChatGPT가 완전한 증명을 주장했으나, 새로운 세션에서 순환 논증이 드러남.
4	오타 수정을 통한 근거 확보	동료 검토된 참고 문헌의 모델 발견 오류가 저자들에 의해 확인되어 신뢰도 상승.
5	폐기 및 복구 전략	노이즈가 많은 초안 대부분을 폐기하고, Hahn 급수의 유한 차수 소수성(finite-degree primality)에 관한 일관된 결과를 유지.
6	형식 검증	두 개의 독립적인 Lean 에이전트가 유한 차수 결과와 이후 전체 정제 추측을 인증함.
7	증명 맵 도구	사용자 정의 스크립트가 Mermaid 다이어그램과 대화형 웹 UI를 생성하여 의존성 구조를 시각화함.

최종 Lean 증명

증명은 GitHub 저장소 gaearon/conway-refinement 의 ConwayRefinement/Standalone에 있습니다.
각 독립형 파일은 Mathlib만 임포트하여 자체 완결성을 보장합니다.
감사를 통해 다음을 확인했습니다:
- 추가 공리가 도입되지 않음.
- 임포트가 독립형 정책을 준수함.
- 모든 진술에 대응하는 Lean 증명이 존재함.
Lean 커널에 의해 컴파일된 증명 인증서가 추측의 진술을 확인합니다(컴파일 영상 링크 참조).

배운 점

바이브 vs 이해 – 프로젝트는 깊은 개인적 전문 지식 없이도 성공했지만, 표류를 감지하기 위해 지속적인 "바이브 체크"가 필요했습니다.
에이전트 규율 – 배경 형식화와 새로운 결과를 위한 별도의 Lean 에이전트를 사용하여 안정적인 코드의 오염을 방지했습니다.
감사 인프라 – 독립형 폴더, 모듈 계층 검사, 공리 린터는 검토자의 신뢰를 얻는 데 결정적이었습니다.
인간 피드백 – 수학자들에게 오타 수정에 대해 이메일을 보낸 것은 현실적인 검증과 신뢰성을 확보하는 발판이 되었습니다.
모델 상호보완성 – Claude는 구조화된 Lean 생성에 뛰어났고, ChatGPT는 탐색적 수학과 비판에 더 능숙했습니다.
토큰 경제 – 더 유도된 워크플로우를 사용하면 비용을 5~10배 절감할 수 있습니다.
증명 제시 – Lean 코드를 읽기 쉬운 PDF로 번역하는 것은 여전히 병목 현상이며, 대화형 증명 맵이 그 간극을 메우는 데 도움이 되었습니다.

커뮤니티 반응 (선택된 HN 댓글)

"이 접근 방식은 마법과 요술의 차이처럼 느껴집니다. 저자는 주문을 완전히 이해하지 못한 채 강력한 존재(LLM)를 소환하고 있습니다." – @gbjcantab

"저는 수학자가 아닙니다. '모든 틈새에 생성(spawn in every gap)' 규칙이 어떻게 유리수를 넘어선 결과를 가져오나요?" – @rlue

"이 워크플로우는 다중 에이전트, 적대적 테스트, 지속적 통합이라는 실제 엔지니어링 프로세스를 반영합니다." – @spongebobstoes

"증명은 인상적이지만, 독립적인 검증 없이는 수학계는 여전히 회의적일 것입니다." – @patcon (교수의 리뷰 링크 포함).

미해결 질문

검증 – 독립적인 수학자들이 Lean 코드를 감사하고 논리적 단계를 확인해야 합니다.
단순화 – 현재 증명 길이는 매우 깁니다. 향후 생성된 증명 맵을 사용하여 압축할 수 있을 것입니다.
일반화 – 동일한 다중 에이전트 파이프라인을 도메인 전문 지식 없이 다른 미해결 문제에 적용할 수 있을까요?
모델 정렬 – LLM 제공업체는 "환각" 정리를 장려하지 않으면서 엄격한 수학적 연구를 어떻게 더 잘 지원할 수 있을까요?

저자는 증명 저장소와 Zulip 채널에서 비판, 버그 보고 및 토론을 환영합니다.