비전공자 1년차가 AI 6모델 20라운드로 콜라츠 추측에 도전한 정직한 실패기

콜라츠를 푼 건 아니었다. 대신, AI가 어디서 발명 흉내를 내고 어디서 검증이 필요한지는 아주 선명하게 드러났다.

나는 원래 이 글을 “AI가 60년 난제를 풀 수 있을까?”라는 질문으로 시작하려고 했다. 결론부터 말하면, 이번 프로젝트에서 콜라츠 추측 자체는 못 풀었다. 그런데 이상하게도 그 실패가 제일 값졌다. 왜냐하면 이번 6시간, 20라운드, 약 50번의 워커 spawn 동안 정말로 확인한 건 “AI가 수학을 풀 수 있느냐”가 아니라 “AI가 어디서 잘못된 새 이론을 만들어내고, 어디서 진짜 검증이 필요한지”였기 때문이다.

우리가 실제로 한 것

먼저 숫자부터 정리하자. 이 프로젝트는 로맨틱한 한 번의 돌파가 아니라, 꽤 집요한 반복이었다.

중요한 건 “얼마나 오래 돌렸나”가 아니다. 더 중요한 건, 같은 질문을 여러 모델과 여러 워커에게 던졌을 때 어떤 패턴이 반복되는지였다. 이 프로젝트의 내부 노트는 아주 솔직하다. 콜라츠 추측 본체는 못 풀었다. 대신 새 이론처럼 보였던 것들이 반복적으로 무너졌고, 그 과정에서 Skeptic Agent의 필요성이 거의 증명 수준으로 드러났다.

시작점은 단순했다

시작은 정말 단순했다. “AI가 60년 난제를 풀 수 있을까?”라는 호기심이었다. 보통 이런 종류의 질문은 두 갈래로 끝난다.

1. 아무 성과 없이 흩어진다.
2. 운 좋게 작은 결과 하나를 건진다.

이번 프로젝트는 이상하게도 둘 다였다. 큰 문제는 못 풀었지만, 작은 결과는 꽤 단단하게 남았다. 특히 Lean 4에서 실제로 컴파일된 정리 두 개는 “말만 그럴듯한 주장”과 “기계가 통과한 주장” 사이의 간격을 아주 선명하게 보여줬다.

그 간격이 바로 이 글의 핵심이다.

반복된 패턴: 새 이론처럼 보였지만, 대부분은 아니었다

내부 노트에서 가장 흥미로웠던 부분은, AI가 무언가를 계속 “새로운 개념”처럼 만들어낸다는 점이었다. 문제는 그 새로움의 상당수가 실제 새 이론이 아니라는 데 있었다.

대표적으로 반복된 패턴은 대략 이랬다.

1. AI가 그럴듯한 이름을 붙인다.
2. 수식이나 용어가 새로워 보인다.
3. Skeptic Agent가 검토한다.
4. 알고 보니 기존 레마의 재명명, 윈도우 선택 아티팩트, 또는 finite-size artifact다.

내부 기록에 남은 반증 시도만 봐도 비슷한 결말이 반복됐다.

• ψ Phantom Spectral Index — 결국 Lemma D의 재명명에 가까웠다.
• Bi-adic Flow Φ — Skeptic가 일찍 걸러냈다.
• CF Resonance Δ_CF — finite-size artifact로 판정됐다.
• α = 0.0125 universal — 윈도우 선택 결과였다.
• T(N) ≤ 10.22·ln²(N) — N=27 fitting에서 출발했지만, 그 자체로 곧바로 일반 법칙이 되지는 않았다.

이런 패턴은 꽤 중요하다. 왜냐하면 AI가 잘하는 건 “그럴듯한 구조를 빨리 뽑는 것”이지, 그 구조가 진짜 새 것인지 스스로 구별하는 건 아니기 때문이다.

왜 Skeptic Agent가 필수였나

이번 프로젝트에서 제일 값진 설계는 사실 모델이 아니라 Skeptic Agent였다.

AI는 제안하는 데에는 강하다. 그런데 그 제안이 진짜 새롭고, 일관되고, 반례에 견디는지 판단하는 데는 약하다. 그래서 한쪽에서 발명처럼 보이는 말을 내놓고, 다른 쪽에서 냉정하게 뜯어보는 구조가 필요했다.

Skeptic Agent가 없었다면 어떤 일이 벌어졌을까?

• 이름만 바뀐 기존 아이디어를 새 정리처럼 착각했을 가능성이 높다.
• 특정 구간에서만 맞는 패턴을 보편 법칙으로 확대했을 가능성이 높다.
• 반증보다 포장에 더 시간을 썼을 가능성이 높다.

반대로 Skeptic Agent가 들어가면 좋은 점은 분명하다.

• 새 주장과 재명명을 빠르게 분리한다.
• 작은 데이터셋의 우연을 일반화하지 못하게 막는다.
• 반례 탐색을 자동화해 발명 속도보다 검증 속도를 끌어올린다.

이건 수학 연구만의 얘기가 아니다. 지금 AI 도입이 어려운 이유 대부분이 여기 있다. 생성 자체는 쉬워졌는데, 검증과 반증이 여전히 비싸다. 그래서 진짜 병목은 모델이 아니라 검증 루프다.

그래도 남은 건 있다: 기계가 실제로 통과한 것들

실패만 있었던 건 아니다. 다만 남은 것은 “대형 정리”가 아니라 “작지만 확실한 검증” 쪽이었다.

내부 리서치 노트와 Lean 4 파일에서 확인된 건 대략 이런 것들이다.

• N=871에 대한 phantom 실현 정리
• N=131,775에 대한 phantom 실현 정리
• reverse Collatz tree growth rate에 대한 이론적 도출
• phantom necessary condition 형태의 관찰
• 특정 범위에서의 phantom desert 관찰

여기서 가장 중요한 포인트는, 이 결과들이 모두 같은 급의 성과는 아니라는 점이다. 어떤 건 형식 검증된 작은 사실이고, 어떤 건 경험적 관찰이고, 어떤 건 기존 문헌과 겹칠 가능성이 있다. 그런데 바로 그 차이를 명확히 구분하는 게 이번 프로젝트의 성숙한 부분이었다.

즉, “AI가 뭔가 했다”가 아니라, “AI가 한 것 중 무엇이 실제로 검증됐는지”를 분해해냈다.

그게 진짜 가치다.

왜 Lean 4가 중요했나

Lean 4는 이번 프로젝트에서 일종의 현실 검증 장치였다.

대화형 모델은 말하기를 잘한다. 그런데 말은 말일 뿐이다. 반면 Lean 4에서 컴파일이 통과하면 적어도 그 문장 안에서는 기계가 이해 가능한 수준의 엄밀함을 얻는다.

이 프로젝트에서 Lean 4가 가진 의미는 거창하지 않다. 오히려 소박하다.

• 작은 정리라도 형식화되면 남는다.
• 인간의 감각적 확신과 기계 검증을 분리할 수 있다.
• 나중에 다시 읽을 때 “정말 증명됐는가”를 확인할 기준점이 생긴다.

이건 수학에서만 유효한 태도가 아니다. AI 시대의 거의 모든 작업에 동일하게 적용된다. 말이 아니라 검증된 결과를 남겨야 한다. 특히 에이전트가 많아질수록 더 그렇다.

AI는 무엇을 잘하고, 무엇을 못하나

이번 프로젝트는 결국 LLM의 능력에 대한 메모이기도 했다.

잘하는 것

• 계산 검증
• brute force/탐색
• 후보 정리의 빠른 생성
• 재서술과 재구성
• 작은 형식 명제 작성

못하는 것

• 새 수학적 추상화의 진짜 본질 파악
• 이름만 바꾼 것과 진짜 새 개념의 구별
• 장기적 인내가 필요한 이론 수렴
• 반례를 만나도 스스로 포기하지 않는 태도

그래서 나는 이제 “AI가 연구를 대신한다”는 표현을 별로 믿지 않는다. 더 정확한 말은 이거다.

AI는 연구의 속도를 올려주지만, 연구의 진위 판정까지 대신해주지는 않는다.

그 차이를 모르고 쓰면, 결과는 화려해 보여도 금방 모래처럼 무너진다.

이 프로젝트에서 가장 솔직했던 순간

솔직히 말하면, 나는 중간중간 꽤 여러 번 “이제 뭔가 새 걸 잡았나?”라고 생각했다.

그런데 거의 매번 결과는 비슷했다.

• 새 이론이라고 부르기엔 너무 기존 개념의 변주였다.
• 경험적으로 맞아 보여도, 범위를 넓히면 금방 깨졌다.
• 좋은 이름을 붙이는 것과 좋은 정리를 만드는 것은 다르다.

이걸 반복해서 확인한 것만으로도 충분히 의미 있었다. 왜냐하면 AI가 만들어내는 착시를 몸으로 배웠기 때문이다.

그리고 그런 착시를 막아주는 장치가 바로 Skeptic Agent였다.

그래서 이번 글의 진짜 제목은 이것이다

표면적으로는 “콜라츠 추측에 도전한 실패기”지만, 사실 더 정확한 제목은 이거에 가깝다.

AI 다중 에이전트 연구에서, 발명보다 검증이 먼저라는 걸 증명한 기록

이 문장이 조금 더 본질적이다.

우리는 콜라츠를 못 풀었다. 맞다. 하지만 그 과정에서 다음은 명확해졌다.

• 모델은 제안을 잘한다.
• Skeptic은 착시를 잘 자른다.
• Lean 4는 작은 사실을 실제로 고정한다.
• 연구의 품질은 모델 하나가 아니라 검증 루프 전체에서 결정된다.

내가 다음에 같은 일을 한다면

같은 프로젝트를 다시 한다면, 나는 처음부터 이렇게 설계할 것이다.

1. 발명용 에이전트와 반증용 에이전트를 분리한다.
2. 작은 형식 검증을 초반부터 끼워 넣는다.
3. 결과를 크게 말하기 전에, 어떤 것이 검증됐는지부터 표준화한다.
4. 새 이름을 붙이기 전에 기존 문헌과의 중복 가능성을 먼저 점검한다.
5. 실패 로그를 남겨서, 나중에 같은 착시를 다시 반복하지 않게 한다.

이 다섯 가지가 있으면 AI 연구는 훨씬 덜 허세가 된다.

한 줄 결론

콜라츠 추측 자체는 못 풀었다. 하지만 그 실패 덕분에, 나는 AI 다중 에이전트 연구에서 진짜 중요한 것이 “더 센 모델”이 아니라 “더 센 검증”이라는 걸 아주 분명하게 봤다.

그리고 그건 실패가 아니라, 다음 연구를 더 낫게 만드는 데이터다.

참고한 문서와 배경

• Terence Tao, Almost all Collatz orbits attain almost bounded values
• Terence Tao, The Notorious Collatz conjecture
• 내부 리서치 노트: 00-README-FINAL.md
• 내부 최종 노트: outputs/00-FINAL-research-note-v11.md
• Lean 4 검증 파일: lean_project/collatz_proofs/CollatzProofs/CollatzPhantom.lean

이 글은 “정답”보다 “검증된 실패와 작은 확실성”을 남기기 위한 기록이다. 그래서 더 길게 썼다.