Dan Abramov, 한 달간 Claude로 콘웨이 세분화 추측 Lean 증명 작성... 수학자 독립 검증은 아직
- React 개발자로 알려진 Dan Abramov가 한 달간 개인 시간과 대량의 유료 토큰을 쏟아 Claude로 콘웨이의 세분화 추측(1976년 제기)의 Lean 증명을 얻었다고 공개함. 추측 내용은 옴니픽 정수에서 ab = cd이면 a = ef, b = gh, c = eg, d = fh를 만족하는 옴니픽 정수 e, f, g, h가 존재한다는 것임.
- 증명은 수학자의 독립 검증을 받지 않음. Palomar 레지스트리(PALOMAR-2026-09-03-000002, version 1) 기계 검사를 통과했고 Lean 커널 버그에 의존하지 않는다는 전제에서 맞을 가능성이 높다고 저자가 밝힘.
- 문제는 Claude가 골랐음. 초현실수 영역에서 L'Innocente–Mantova 연구(2024)가 콘웨이 1976 추측과 동치로 환원한 문제를 지목했고, 저자는 Claude에게 끌리는 문제를 직접 고르라고 지시함.
- 증명 코드는 GitHub gaearon/conway-refinement에 공개됨. 글에 쓰인 초현실수 삽화는 Joel David Hamkins가 그렸고, 초현실수는 공집합에서 시작하는 단일 생성 규칙만으로 실수, 서수, ω^ω 같은 수까지 만들어냄.
- 해커뉴스 댓글에서는 글의 초현실수 설명이 불친절하다는 지적과 함께, 유한한 LLM은 모든 정리를 증명할 수 없다는 계산이론 반론(정지 문제, busy beaver)과 Gowers의 문제 해결 대 개념 이해 논쟁이 이어짐.
Hacker News opinions
둘째 날에 갑자기 -1이랑 1이 튀어나오는 부분에서 나도 완전히 멈췄음. 나도 수학은 글렀나 봄.
설명이 그냥 나쁨. 초현실수는 초현실수의 집합 두 개로 정의되는 건데, 'nothing'은 그냥 공집합을 뜻하는 말이고 0을 가리키는 게 아님. 이해하고 싶으면 Conway의 On Numbers and Games를 읽는 게 훨씬 낫더라.
그림 하나 보니까 확실히 이해가 되더라.
규칙을 제대로 안 써놨음. 어느 수를 넣는지 안 알려주니까 이런 절차로 유리수만 나오는 거 아닌가 싶었음.
nothing이랑 0이 뭐가 다른지 한참 고민했는데 그냥 넘어가기로 했음.
L|R 구성부터 차근차근 보면 아무 수 없이 시작해서 ∅|∅가 0이 되고, 거기서 다시 새 수가 나옴. 처음부터 이렇게 친절하게 썼으면 좋았을 듯.
석 달 뒤에 에이전트 떼가 서로 통신할 수 있게 되면 이런 작업도 훨씬 쉬워질 텐데. 이번 건 그래도 대단한 거 맞음.
무한 원숭이 정리랑 같은 논리임. 토큰이 무한하면 유한한 LLM 에이전트도 언젠가 모든 정리를 찾긴 할 거임. AI는 그냥 원숭이 역할.
그건 사람도 마찬가지 아님? 생각할 시간이 무한하면 사람도 모든 정리를 풀 텐데. AI가 도대체 뭘 해야 똑똑하다고 인정하는 거임?
아니 그건 틀렸음. 유한한 LLM이 모든 정리를 풀 수 있으면 busy beaver 수열이 계산 가능해지고, 그러면 정지 문제가 결정 가능해짐. 어떤 유한 프로그램에도 증명 못 하는 참인 정리가 반드시 존재함. 사람이 프롬프트를 넣는 순간 그게 추가 정보원이 돼서 한계가 풀리는 거고.
Gowers가 쓴 두 문화 글 링크랑 같이 보니까 훨씬 재밌음. 이해는 0, 문제 해결은 100인 프로젝트를 진짜로 해버린 메타 실험이라는 거.
Gowers 글이 올라온 직후에 딱 이 글이 나온 타이밍이 묘함. 마케팅 기계가 잘 돌아가는 것처럼 보이기도 하고.