인간 수학자, 반례 찾기에서 AI에 추월당하다

6 hours ago 1

ChatGPT와 Claude 계열 모델이 불과 몇 주 사이 Erdős의 단위 거리 추측, Grothendieck의 군 스킴 질문, Jacobian Conjecture에 반례를 만들었으며 일부는 Lean으로 검증됨
OpenAI의 Sol은 Erdős 반례와 필요한 전역 유체론 결과를 3주 만에 120만 줄의 Lean 코드로 형식화했으며, 이는 9년간 작성된 mathlib 230만 줄의 절반이 넘는 규모임
Grothendieck의 60년 된 질문에는 Sol이 12쪽짜리 반례를 찾고 Fable이 4시간 만에 1,076줄로 형식화해, 위수 4이지만 4에 의해 소멸하지 않는 군 스킴의 존재를 확인함
자동 형식화는 연구 속도도 크게 높여, Andrew Yang이 약 2주 동안 25만 줄의 Lean 코드를 작성하며 Fermat의 마지막 정리에 필요한 모듈러성 올림 정리 프로젝트를 사실상 완성함
AI가 생성한 비형식적 수학을 그대로 신뢰할 수는 없지만, 추측을 정확한 Lean 명제로 만들면 증명과 반증을 기계적으로 검사할 수 있으며 인간은 반례에서 더 깊은 수학적 통찰을 끌어내야 함

Erdős 단위 거리 추측과 전역 유체론

2026년 5월 20일 ChatGPT가 이산기하학의 Erdős 단위 거리 추측을 반증함
- 1960년대 Golod와 Shafarevich의 깊은 정수론 정리를 이용해 반례를 구성함
- 여러 수학자가 논증을 사전에 검토해 타당하다고 판단했지만, 발표 당시 Lean 형식화는 없었음
5월 26일 필즈상 수상자이자 Logical Intelligence 최고과학책임자인 Mike Freedman이 자사 시스템으로 ChatGPT 논문 전체를 Lean에 자동 형식화했다고 알림
- 형식화된 범위는 Golod–Shafarevich 정리가 Erdős 반례를 함의한다는 명제였음
- 기반이 되는 정수론 정리 자체에는 100쪽 이상이 필요하며, 전역 유체론의 방대한 부분에 의존함
2025년 유체론 형식화 여름학교 이후 1년 동안 국소 사례는 거의 완성됐지만 전역 사례는 미해결 상태로 남아 있었음

6월 26일 OpenAI의 Boris Alexeev가 새 모델 Sol을 유도해, 수학 공리 외에는 아무것도 가정하지 않는 Erdős 반례의 완전한 형식화를 만들었다고 Lean Zulip에 공개함
Sol은 3주 동안 120만 줄의 Lean 코드를 생성함
- 9년에 걸쳐 작성된 mathlib는 230만 줄임
- 코드 품질은 고르지 않았지만, 전역 유체론의 어려운 결과와 수체의 코호몰로지에 관한 비자명한 정리를 실제로 증명함
Lean은 임의 명령을 실행할 수 있는 프로그래밍 언어이므로, 악성 코드 가능성을 고려해 생성 코드를 샌드박스에서 실행함
이 규모와 속도는 대규모 AI 생성 수학 개발이 불가피하다는 판단으로 이어짐

7월 6~10일 열린 Formalizing Fermat 워크숍에는 25명이 참석했지만, 후원사 Logos Research의 자동 형식화 시스템은 동시에 5명만 사용할 수 있었음
모든 참석자에게 한 달짜리 Claude Max 구독을 제공해 Claude Fable을 쓸 수 있게 했고, OpenAI도 한 달짜리 ChatGPT Pro 접근권을 무료로 제공함
- Sol은 7월 9일 출시 예정이었음
- Fable은 7월 7일 종료될 예정이었지만 실제 접근은 유지됨
- 참석자들은 워크숍 5일 중 4일 동안 Sol과 Fable을, 전체 기간에는 Logos 도구를 이용할 수 있었음
Fermat의 마지막 정리 형식화에 필요한 유한 평탄 군 스킴 이론을 개발하기 위해 고전 논문들을 Fable과 ChatGPT에 입력하고 자연어 해설을 작성하게 함
- Logos는 해설에 포함된 한 명제가 거짓임을 찾아 명시적인 반례를 내놓음
- 확인 결과 표준 구성을 기술한 LLM 생성 문서가 잘못돼 있었으며, 사람은 읽는 과정에서 오류를 놓쳤음
- 단순히 논증을 이해하지 못한다고 답하는 대신 논증이 틀렸다는 증명을 제공했다는 점에서 차이가 있었음

UChicago 교수 Akhil Mathew는 모든 위수 (n)의 유한 자유 군 스킴이 (n)에 의해 소멸하는지를 묻는 Grothendieck의 오래된 질문을 AI에 제안함
- Deligne은 가환인 경우를 증명함
- Grothendieck은 밑공간이 reduced인 경우를 증명함
- Rene Schoof가 더 많은 사례를 다뤘고, Emiliano Torti도 전년도 논문에서 더 일반적인 경우를 증명함
워크숍 다음 날인 7월 11일 Sol이 반례를 찾아 12쪽짜리 PDF를 생성함
- 비형식적 결과 대신 전체 Lean 형식화를 요청하자 Fable이 4시간 만에 1,076줄로 자동 형식화함
Lean 파일에 파일 삭제 같은 명령 없이 정리만 담겼는지 먼저 검사한 뒤 노트북에서 컴파일함
- 명제에 mathlib의 개념만 사용됐는지 확인함
- 명제가 실제로 반례의 존재를 나타내는지 점검함
- 증명이 정상적으로 컴파일되는지 검사함
- 전체 검증에는 5분이 채 걸리지 않았음
검증 결과 위수 4이지만 4에 의해 소멸하지 않는 군 스킴이 존재함
Akhil Mathew는 이 반례를 mathlib PR로 제출함
Erdős 반례는 약 100만 줄인 반면 Grothendieck 반례는 약 1,000줄로 훨씬 단순했지만, 60년 된 대수기하학 질문을 기계가 해결한 사례가 됨

7월 14일 Imperial College의 한 교수는 Grothendieck 반례가 쉽게 발견됐다는 사실이 인간이 해당 문제를 충분히 오래 생각하지 않았음을 보여줄 뿐이라고 평가함
박사과정 학생 Andrew Yang은 Fermat의 마지막 정리에 중요한 모듈러성 올림 정리를 Lean으로 형식화하면서 Sol과 Fable을 사용함
- 약 2주 동안 25만 줄의 Lean 코드를 작성함
- 이를 통해 프로젝트를 사실상 완성함
Imperial의 다른 교수는 대학원생들이 Sol과 Fable에 월 200달러를 지불하는 것을 이해하기 어렵다고 봤지만, 이 성과를 확인한 뒤에는 오히려 도구에 월 200달러를 쓰지 않는 박사과정생이 비합리적이라고 판단함
Harvard는 이미 모든 박사과정생, 박사후연구원, 교수에게 Fable 무료 접근권을 제공하고 있었음

Akhil Mathew와 Levent Alpöge는 대수기하학에서 추가 반례를 찾는 방안을 논의했고, Fable이 약 100년 동안 열려 있던 유명 문제인 Jacobian Conjecture의 반례를 찾음
Levent Alpöge는 2026년 월드컵 결승전 도중 해결된 것으로 보이는 결과를 X에 공개함
Akhil Mathew가 새 mathlib PR을 제안했을 때는 Paul Lezeau가 이미 반례를 수동으로 형식화해 DeepMind의 Formal Conjectures 저장소에 PR을 제출한 뒤였음
mathlib에는 수학 추측의 대규모 목록이 없지만, Formal Conjectures 저장소는 이를 보유함
사람이 추측의 뜻을 충실히 담은 Lean 명제에 합의하면, AI가 생성한 코드가 그 추측을 증명하거나 반증하는지 확인하는 작업은 간단해짐