AI와 Lean을 사용하여 Conway의 세분화 추측을 증명한 방법

TL;DR

저는 수개월간의 프롬프팅, 방대한 토큰 실험, 그리고 Lean 형식화를 거쳐 omnific integers에 대한 Conway의 세분화 추측(refinement conjecture)을 기계적으로 검증된 증명으로 생성하는 다중 에이전트 AI 연구소를 구축했습니다. 이 증명은 Palomar 레지스트리를 통과하고 비공식적인 전문가 검토를 거쳤으나, 아직 독립적인 검증은 이루어지지 않았습니다.

Conway의 세분화 추측이란 무엇인가

Conway의 추측(1976)은 초현실 수 체계의 정수 부분인 omnific integers에 관한 것입니다. 이 추측은 *세분화 속성(refinement property)*을 주장합니다. omnific integers a, b, c, d에 대해 ab = cd라면, 다음을 만족하는 omnific integers e, f, g, h가 존재합니다.

[ a = ef,\quad b = gh,\quad c = eg,\quad d = fh. ]

일반 정수에서는 이것이 자명합니다(예: 210 = 10·21 = 6·35는 2·5·3·7로 세분화됨). 이 추측은 ω, 2ω, ω^ω와 같은 무한 및 무한소 값, 심지어 -ω/7과 같은 "전체" 무한소까지 포함하는 훨씬 더 풍부한 omnific integers에서도 동일한 인수 재배열이 성립하는지 묻습니다.

AI 기반 워크플로우 개요

이 프로젝트는 5주간의 단계로 진행되었으며, 각 단계마다 에이전트, 역할, 그리고 Lean과의 상호작용을 개선했습니다.

1주차 – 순진한 원샷 시도

Claude에게 추측에 대해 "돌파구를 마련하라"고 프롬프트함.
Claude는 일관성이 없고 검증 불가능한 전문 용어로 가득 찬 긴 산문을 생성함.
ChatGPT의 "회의적인" 페르소나로 전환하여 짧고 그럴듯한 보조 정리를 얻었으나 여전히 일관된 증명은 나오지 않음.

2주차 – 다중 에이전트 연구소

결정론적 토큰 사용을 위해 Codex를 로컬에 다운로드함.
명시적 역할을 가진 에이전트 생성: PM(프로젝트 관리자), Math(아이디어 생성기), Red(적대적 검토자), Random(탐색적), Lean(형식화).
에이전트들은 공유 "카페테리아" 채널을 통해 소통하며, PM이 병합을 조정함.
이 워크플로우는 방대한 TeX 코퍼스를 생성했으나 검증된 새로운 결과는 없었음.

3주차 – 막다른 길과 토큰 고갈

Lean 형식화를 위해 다시 Claude를 투입; 모델은 자신의 주장을 인증했다가 나중에 반박하는 과정을 반복함.
TeX 스택이 약 30개의 "논문"으로 늘어났으며, 작은 실수 하나가 전체 탑을 무너뜨릴 위험이 있었음.
유망해 보이는 전체 증명이 나타났으나, 정밀 감사 결과 순환 의존성이 발견되어 아직 증명이 존재하지 않음이 확인됨.

4주차 – 현실에 기반하기

동료 검토를 거친 참고 문헌(L’Innocente–Mantova 2024)의 구체적인 오류를 검증하는 데 집중함. 저자들과 여러 오타를 확인하며 모델이 실제 문제를 찾아내는 능력에 대한 신뢰를 구축함.
이전 코퍼스를 모두 폐기하고 ChatGPT에게 수학적으로 건전한 내용을 살려달라고 요청함.
문헌에서 유한 차수 소수성(finite-degree primality) 결과를 발견했으며, 검증 후 이것이 새로운 정리임을 확인함.

5주차 – 통합 및 최종 증명

첫 번째 Lean 에이전트가 기존 문헌만 처리하는 동안, 새로운 결과를 인증하기 위해 두 번째 독립적인 Lean 에이전트를 구축함.
엄격한 독립형(standalone) 폴더(내부 임포트 없음)를 도입하고 추가 공리, 모듈 계층화, 증명 크기에 대한 자동 감사를 수행함.
증명 맵(Mermaid 다이어그램)을 생성하여 의존성을 시각화하고 모델이 불필요한 가지를 제거하도록 함.
여러 번의 "즐겁게 하라"는 프롬프트 반복 끝에, 에이전트들은 추가 공리 없이 컴파일되는 전체 세분화 추측의 독립형 Lean 인증서를 생성함.

주요 기술적 산출물

산출물	설명
GitHub repo – `gaearon/conway-refinement`	Lean 소스, TeX 초안, 도구 스크립트 포함.
Palomar registry entry – `PALOMAR-2026-09-03-000002`	Lean 커널이 증명을 수락했다는 기계적 검증.
Standalone folder	Mathlib만 임포트하는 파일들로, 각 500줄 미만의 사람이 읽을 수 있는 문장 보장.
Proof map website – `gaearon.github.io/conway-refinement`	증명에 대한 의존성 트리의 대화형 Mermaid 다이어그램.
Custom tooling – `subverso` 속성 주석기, 모듈 시스템 린터, Lean Comparator 통합	깔끔한 모듈 계층화를 강제하고 숨겨진 공리를 방지.

배운 점 (결론부터)

AI는 저자가 수학을 이해하지 못해도 심오한 미해결 문제에 대한 기계적으로 검증된 증명을 생성할 수 있지만, 워크플로우에는 엄격한 엔지니어링 가드레일, 적대적 감사, 빈번한 "폐기 후 재구축" 주기가 필요함.
탐색적 수학에서는 ChatGPT가 Claude보다 유용했으나, 구체적인 목표가 주어졌을 때 결정론적인 Lean 코드 생성에는 Claude가 뛰어났음.
신뢰할 수 있는 문헌과 추측성 결과를 위한 별도의 Lean 파이프라인은 오염을 방지하고 감사를 관리 가능하게 함.
저수준 오류(예: 원본 논문의 오타)에 대한 인간의 검증은 모델의 출력에 대한 신뢰를 구축하고 협업의 발판을 제공함.
증명 맵 시각화와 엄격한 모듈 격리는 모델의 해석 가능성을 크게 향상시켜 에이전트가 "헛소리" 가지를 제거하도록 함.
토큰 비용이 엄청남 – 전체 실행에 약 400억 토큰(약 4만 달러)이 소요됨; 더 나은 조정을 통해 이를 5~10배 줄일 수 있음.

대표적인 커뮤니티 피드백

"이 과정은 저자가 수학을 제대로 배우지 못했지만 모델이 힘든 일을 다 해내는 퍼포먼스 아트 프로젝트처럼 느껴집니다." – m-steffen, HN 댓글

"ChatGPT의 회의적인 페르소나가 Claude의 거창한 원샷 시도보다 훨씬 생산적이었습니다." – nphardon, HN 댓글

"증명 맵과 Mermaid 다이어그램은 모델이 증명의 형태를 파악하고 단순화를 제안하는 데 도움을 주었습니다." – 저자 본인의 관찰

미해결 문제 및 다음 단계

독립적인 수학적 검토 – 이 증명은 아직 초현실 수 분야의 전문가들에 의해 검토되지 않았으므로 커뮤니티 검증이 필수적입니다.
단순화 – 현재 Lean 코드에는 많은 보조 정리가 포함되어 있습니다; 더 짧고 개념적인 증명이 수용에 도움이 될 것입니다.
일반화 – 이 워크플로우를 다른 미해결 문제에 적용할 수 있습니다; 템플릿 저장소를 준비 중입니다.
비용 절감 – 더 나은 프롬프팅 전략과 토큰 효율적인 에이전트를 개발하여 대규모 AI 기반 수학을 더 접근하기 쉽게 만들 것입니다.

최종 요약

여러 LLM 에이전트를 조정하고, 엄격한 Lean 형식화를 강제하며, 환각된 수학을 반복적으로 제거함으로써 Conway의 세분화 추측에 대한 기계적으로 검증된 증명을 생성할 수 있었습니다. 이 결과는 AI 보조 정리 증명이 저자의 전문 지식을 훨씬 뛰어넘는 문제에도 실현 가능함을 보여주지만, 동시에 정확성과 신뢰성을 보장하기 위해 규율 있는 엔지니어링, 적대적 감사, 그리고 인간의 협업이 필수적임을 강조합니다.