Conway의 추측을 바이브 코딩으로 증명해 봤다

수학 비전문가가 약 한 달간 AI 에이전트와 Lean을 활용해 50년 된 Conway의 세분화 추측에 대한 형식 증명을 얻음. 기계적 검사는 통과했지만, 수학자들의 독립 검증은 아직 받지 않음 AI에게 한 번에 증명을 맡기거나 여러 에이전트가 서로 검토하게 하는 것만으로는 부족했음. 검증되지 않은 결과를 쌓으면서 순환 논증과 비표준 용어가 늘어났고, 증명했다고 여긴 결과가 반복해서 무너짐 돌파구는 기존 논문과 새로운 결과의 형식화를 분리하고, 수학적 탐색보다 Lean 검증이 몇 시간만 뒤처지도록 작업을 조정한 데 있었음 증명의 정확성과 사람이 이해할 수 있는 설명은 별개였음. Mathlib만 사용하는 독립 명제, 공리와 의존성 감사, 표준 용어 정비, 증명 지도를 통해 검토 가능성을 높임 복구한 로그에 대한 AI 추정치는 약 400억 토큰, 현재 API 가격 환산 비용은 약 4만 달러임. 전문지식 없이도 상당한 진전을 이뤘지만, 모델의 이탈을 막는 프로젝트 관리와 실제 수학자의 피드백이 중요했음 얻은 증명과 현재 검증 상태 목표는 John Conway가 50년 전에 제안한 세분화 추측(refinement conjecture) 임. 전능정수(omnific integers)에서 ab = cd이면 a = ef, b = gh, c = eg, d = fh를 만족하는 전능정수 e, f, g, h가 존재한다는 명제임 공개된 Lean 증명은 Palomar registry의 기계적 검사를 통과함 Lean과 해당 분야에 익숙한 몇몇 사람은 형식화한 명제가 올바른 것으로 보인다고 평가함 수학자들의 독립 검증은 아직 없으며, Lean 커널의 버그에 의존하지 않는다는 전제 아래 증명이 맞을 가능성이 높다고 판단하고 있음 정확하다고 판단하는 근거를 공개하고 반박을 요청함 출발점은 AI의 수학 성과와 “돌파구를 만들어라”라는 밈을 보고, 수학 비전문가도 미해결 문제를 골라 최신 모델로 풀 수 있는지 시험해 보려는 호기심이었음 첫날: 초현실수와 문제 선택 초현실수(surreal numbers)는 Conway가 만든 수 체계로, 모든 실수와 순서수, 75 + ω×3 + 1/ω 같은 조합을 포함함 풍부한 수 체계가 기존 수 사이의 모든 빈틈에 새 수를 만든다는 하나의 규칙에서 출발함. 전체의 왼쪽과 오른쪽도 빈틈으로 취급함 첫날에는 아무것도 없는 사이에서 0이 생김 둘째 날에는 −1, 1, 셋째 날에는 −2, −1/2, 1/2, 2가 생기고,...