Conway의 추측을 바이브로 증명해 봤습니다

본문

이 글은 수학을 전공하지 않은 개발자가 대규모 언어 모델(LLM)과 Lean을 이용해 John Conway가 1976년에 제기한 것으로 소개되는 Conway의 정제 추측(Conway’s refinement conjecture)에 도전한 과정을 기록합니다. 저자는 몇 달 동안 자유 시간과 막대한 토큰을 사용해 최종적으로 추측의 Lean 증명을 얻었다고 말하지만, 수학자들의 독립적인 검증은 아직 받지 못했습니다. 다만 Palomar registry의 기계적 검사를 통과했고 Lean과 해당 분야를 함께 아는 몇몇 사람에게서 명제 자체가 타당해 보인다는 평가를 받았다고 합니다. 따라서 Lean 커널의 버그에 의존하지 않는다는 전제에서 증명이 맞을 가능성이 있다는 수준으로 제시합니다.

문제의 배경: surreal number와 omnific integer

저자는 Claude에게 surreal number 분야의 미해결 문제를 골라 달라고 요청하면서 이 프로젝트를 시작합니다. Surreal number는 Conway가 고안한 수 체계로, 실수와 ordinal number를 모두 포함하고 무한히 크거나 작은 수, 그리고 이들이 결합된 형태까지 다룹니다. 생성 규칙은 지금까지 만들어진 모든 수 사이의 틈을 찾아 그 사이에 새로운 수를 계속 넣는 방식입니다. 아무것도 없는 양쪽의 틈에서 0이 태어나고, 다음 단계에는 0의 왼쪽과 오른쪽에 각각 -1과 1이 생깁니다. 이후 -2, -1/2, 1/2, 2와 같은 수가 추가되며, 이 과정을 무한히 반복하면 실수뿐 아니라 ω, 1/ω 같은 무한대와 무한소도 나타납니다.

Conway의 추측이 다루는 omnific integer는 surreal number 중 정수에 해당하는 부분입니다. 여기에는 3이나 -5 같은 일반적인 정수뿐 아니라 ω, 2ω, ω^ω, -ω/7처럼 무한히 크거나 일반적인 의미에서는 낯선 수들도 포함됩니다. 추측의 형식은 다음과 같습니다. ab = cd라면, a = ef, b = gh, c = eg, d = fh를 만족하는 omnific integer e, f, g, h가 존재한다는 주장입니다. 즉 두 곱이 같을 때 각 인수를 더 작은 조각으로 분해하면, 양쪽 곱이 사실상 같은 네 조각을 서로 다르게 묶은 결과라는 내용입니다.

일반 정수에서는 이 성질이 자연스럽습니다. 예를 들어 10 × 21 = 6 × 35는 10 = 2 × 5, 21 = 3 × 7로 분해한 뒤 2 × 3 = 6, 5 × 7 = 35로 재조합한 결과로 볼 수 있습니다. 그러나 무한대를 포함하는 수에서는 정수에서 당연하게 보이는 인수분해 구조가 그대로 유지된다고 보장할 수 없습니다. Conway는 omnific integer에도 이런 정제 구조가 남아 있다고 추측한 것입니다.

처음의 접근과 LLM의 그럴듯한 오류

Claude는 이 문제를 L’Innocente–Mantova의 연구와 연결하면서, K((ℝ^≤0))에서 무한 지지(infinite support)를 가진 모든 기약 원소가 소수인지 묻는 문제와 Conway의 추측이 정확히 동치라고 설명했습니다. 그러나 저자는 나중에 Claude의 “문제가 완벽하게 축약됐다”는 설명이 틀렸으며, 실제 증명에는 그보다 더 많은 작업이 필요했다는 사실을 알게 됩니다.

처음에는 Claude에게 논문을 읽히고 반례를 찾거나 추측을 증명하도록 직접 지시했습니다. 하지만 Claude는 “stage-1 obstruction”, “designed resonance”, “frontier data”, “transversality heuristic” 같은 표현을 사용하며 수학적 근거가 충분히 제시되지 않은 장황한 설명을 만들어 냈습니다. 저자는 이를 실제 수학적 주장이라기보다 작업을 정당화하기 위해 만들어 낸 전문용어와 과장된 서술에 가깝다고 판단했습니다. 내용이 맞는지 직접 판별할 수 없었을 뿐 아니라, 다른 수학자에게 검토를 맡길 수 있을 정도로 일관된 형태도 아니었다고 합니다.

이에 저자는 ChatGPT를 사용해 Claude가 만든 자료를 비판하게 했습니다. ChatGPT는 만들어진 용어, 과장된 결론, 사소한 결과를 중요한 발견처럼 포장한 부분, 잘못된 추론 등을 지적했습니다. 이후 저자는 ChatGPT 세션을 복제하고, 한 세션에서 나온 결과를 메모리 없이 새 세션에 넣어 검토하게 하며 여러 실행에서 살아남는 아이디어를 찾았습니다. 세션을 포크해 서로 다른 결과를 합치고, 연결점을 찾아 다음 연구 방향을 제안하게 하는 방식도 사용했습니다.

Codex 기반 다중 에이전트 연구실

수작업으로 세션을 관리하기 어려워진 뒤에는 Codex를 로컬에서 실행하고 역할별 에이전트를 구성했습니다. “PM” 에이전트는 Conway의 추측이라는 목표를 향해 작업을 조정하고 병합했습니다. 여러 “Math” 에이전트는 다음 돌파구를 찾았고, “Red” 에이전트는 수학 에이전트의 제안에서 결함을 찾았습니다. “Random” 에이전트는 정해진 방향에 얽매이지 않고 자유롭게 탐색했으며, “Lean” 에이전트는 합의된 수학적 작업을 Lean으로 형식화했습니다.

Codex의 Goals 기능은 각 세션에 원래 목표를 주기적으로 상기시켰고, 세션 간 메시지 기능은 PM이 작업을 나누고 검토가 끝난 결과만 병합하도록 하는 데 사용됐습니다. 저자는 모든 메시지를 다른 에이전트에게 전달하는 “cafeteria” 에이전트도 만들어 공동 채팅방과 비슷한 환경을 구성했습니다. 흥미로운 아이디어 하나는 증명을 깨뜨리는 역할이던 Red 에이전트에게 창의적인 구성을 요청했을 때 나왔고, Random 에이전트가 이를 발전시켰습니다. 그러나 그 아이디어 역시 나중에 무너졌고, 이후 다시 발견해야 했습니다.

이 워크플로를 며칠간 실행한 결과 거대한 TeX 문서와 많은 Lean 코드가 쌓였지만, Conway의 추측을 성공적으로 닫지는 못했습니다. 모델들은 의미 있는 새 결과가 있다고 주장했지만, 저자는 그 수학을 판별할 수 없었습니다. 에이전트가 과장된 표현으로 흐르거나, 이미 검증했다고 한 결과에서 뒤늦게 오류를 발견하는 일이 반복되면 세션을 종료하고 다시 시작했습니다.

“증명에 가까워진 것처럼 보이는” 실패

프로젝트가 진행되면서 TeX 문서는 하루 만에 약 12개에서 거의 30개로 늘어났습니다. 한 문서에 오류가 있으면 이후 문서 전체가 영향을 받는 구조였지만, Lean 형식화는 그 속도를 따라가지 못했습니다. ChatGPT는 한때 Conway의 추측을 거의 해결했다고 선언할 듯한 내용을 만들었고, 한 파일은 추측 전체를 증명했다고 주장했습니다. 그러나 새 세션이 이를 검토하는 과정에서 필요한 검사를 거치지 않고 대상을 구성한 순환적인 문장이 발견됐습니다. 저자가 엄밀히 복구할 수 없다면 중단해야 한다고 하자, ChatGPT도 “현재 우리는 증명을 갖고 있지 않다”고 인정했습니다.

이 경험은 생성된 논문 묶음이 실제로는 검증되지 않은 결과를 이미 확립된 사실처럼 인용하는 “사적인 정리 문헌”이 될 수 있음을 보여줬습니다. 저자는 결국 수학의 내용을 이해하지 못한 채 증명을 추진하는 방식이 현명하지 않았을 수 있다고 판단하고 약 일주일 동안 프로젝트를 중단했습니다.

검증 가능한 작은 결과로 방향 전환

재개한 뒤 저자는 Conway의 추측을 바로 풀려는 대신, 참고하던 동료 심사 논문 하나에서 오류를 모두 찾는 작업으로 범위를 좁혔습니다. ChatGPT와 Lean이 찾아낸 오탈자와 작은 결함이 실제로 존재하는지 논문 저자들에게 문의하고, 반복 실행에서도 같은 오류를 재현하는지 확인하려 했습니다. 이 과정에서 일부 수정 사항은 실제 오류로 확인됐지만, Lean의 뒷받침이 없던 몇몇 문제는 저자의 오해로 밝혀졌습니다. 모델이 수학적 설명을 작성할 때 빈틈이 있거나 자체적으로 만든 용어를 설명 없이 사용하는 문제도 계속 나타났습니다.

그럼에도 모델이 기존 논문에서 실제로 고칠 수 있는 오류를 발견했다는 사실은 일정한 신뢰의 근거가 됐습니다. 이후 ChatGPT는 과거 자료 전체를 감사하면서, Conway의 추측에 대한 신뢰할 만한 증명은 없지만 여러 문서에 흩어져 있던 결과 중 유한 차수 부분이 특정 주환(principal ring)이 다항식환(polynomial ring)임을 직접 보이는 흥미로운 결과로 정리될 가능성이 있다고 제안했습니다. 저자는 이 주장의 새로움을 인간 수학자에게 확인했고, 실제로 일관된 수학적 결과가 LLM이 만든 비표준 용어와 과장된 문서들 속에 묻혀 있었다고 설명합니다. ChatGPT 스스로도 전체 자료 가운데 보존할 만한 수학은 약 10~15%, 새로운 기여가 아닌 일반적인 수학은 35~45%, 거대한 정리 체계와 조건부 가정을 진전처럼 포장한 “bullshit”은 40~50% 정도라고 평가했습니다.

이에 저자는 다시 연구실을 구성하되, 기존 문헌을 형식화하는 Lean 에이전트와 새로 얻은 유한 차수 소수성 결과를 형식화하는 Lean 에이전트를 분리했습니다. 하나의 에이전트가 검증된 수학과 미성숙한 자체 결과를 함께 다루면서 추상화와 오류를 뒤섞었던 이전의 문제를 피하기 위해서입니다. 새 수학 에이전트들은 결과를 Conway의 추측으로 확장하려 했고, Red 에이전트는 계속해서 인간 연구자의 결과를 반박하는 역할을 맡았습니다. 이 글의 핵심은 AI가 곧바로 미해결 수학 문제를 해결했다는 선언보다, LLM의 탐색 능력과 Lean의 기계적 검증을 결합하려면 중간 결과를 작은 단위로 분리하고 인간 연구자에게 확인받아야 한다는 과정에 있습니다.

Hacker News 반응

• @howunfortunate — “둘째 날에는 ‘아무것도 없는 것과 0 사이’, ‘0과 아무것도 없는 것 사이’라는 두 개의 틈이 있습니다. 여기서 길을 잃었습니다. 저는 공식적으로 수학에 너무 멍청한 것 같습니다.”
• @jdw64 — “저도 똑같이 느낍니다. 멍청이와 더 멍청이 듀오가 되고 싶으신가요? 저는 당신의 친구가 될 수 있다고 믿습니다.”
• @howunfortunate — “룸메이트의 계정으로 프런티어 연구소 인턴에게서 무제한 토큰을 얻은 멍청이와 더 멍청이 듀오가 미니시리즈를 찍는다는 설정입니다. 매 회 과학소설 같은 중대한 돌파구를 만들고, 정체를 밝히지 않은 채 그 결과와 씨름합니다.”
• @DrewADesign — “반전은 이렇습니다. 둘 다 닷컴 버블 붕괴에서 살아남은 회사에 일찍 투자해 둔 상태입니다. 이제 사람들은 그들을 사업 천재라고 숭배하지만, 사실은 운이 좋았던 바보일 뿐입니다. 아첨하는 챗봇들이 마침내 사람들이 말하던 만큼 똑똑하다고 느끼게 해 주고, 과대광고에 취한 팬들이 그들을 떠받들고 있습니다.”
• @dubcanada — “그냥 이 숫자들을 말하거나 쓸 방법이 없다는 뜻이라고 생각합니다. 그래서 숫자를 쓰는 방법을 새로 만들고(-1과 1), 계속 진행하는 것입니다. 숫자 자체는 중요하지 않아서 -1과 1을 아무것으로 바꿔도 됩니다. 위치가 중요하기 때문에 새 가짜 숫자를 -1과 1로 시작하는 편이 더 쉬운 것입니다.”

원문: overreacted.io / 번역·요약: Trawling