AI가 수학 미해결 문제 10개를 건드렸다 — 필즈상 수상자의 인정
OpenAI says an internal model advanced ten open math problems — with formal proofs on GitHub
오픈AI 내부 모델이 수학·이론전산 미해결 문제 10개를 해결·전진시켰다고 발표했고, 형식 증명이 공개돼 검증 가능하다
3줄 요약
- 오픈AI 내부 모델 아스트라(Astra)가 미해결 문제 10개를 해결 또는 크게 전진시켰다고 발표
- 비소픽 군의 존재 증명, 구 채우기 한계 개선 등 — Lean 형식 증명을 깃허브에 공개
- 필즈상 수상자 가워스 '최상급 저널에 주저 없이 추천할 증명' — 자체 발표 너머의 인정
핵심 질문
- AI가 수학 문제를 풀었다는 게 무슨 의미야
- 시험 문제가 아니라 '아무도 답을 모르던' 미해결 문제라는 점이 다르다. 오픈AI는 내부 모델 아스트라가 군론의 비소픽 군 존재 증명, 구 채우기(sphere packing) 한계 개선 등 10개 문제를 해결하거나 크게 전진시켰다고 발표했다. 인류가 답을 몰랐던 질문에 기계가 새 답을 보탠 사례라는 주장이다.
- 발표를 그대로 믿어도 돼
- 이번엔 검증 장치가 다르다. 결과 일부가 Lean이라는 형식 증명 언어로 작성돼 깃허브에 공개됐다 — 형식 증명은 컴퓨터가 논리 단계를 기계적으로 검사하므로 '그럴듯한 오답'이 끼어들 수 없다. 여기에 필즈상 수상자 티머시 가워스가 '최상급 저널에 주저 없이 추천하겠다'고 평가해 외부 인정도 얻었다.
- 이게 일반인한테도 중요한 일이야
- AI 능력의 성격이 바뀌는 신호라서다. 지금까지 AI는 '알려진 지식을 재조합'하는 도구로 평가받았지만, 미해결 문제의 전진은 '새 지식의 생산'에 해당한다. 수학은 정답 검증이 가장 엄격한 분야라 이 경계 돌파의 첫 무대가 됐다 — 다음 무대가 과학·공학이라는 전망이 이 발표의 진짜 무게다.
AI 뉴스의 단골 문장은 "벤치마크에서 몇 점을 받았다"였다. 이번 주는 문장이 달랐다 — "아무도 못 풀던 문제를 풀었다." 오픈AI가 내부 모델 아스트라(Astra)로 수학·이론전산학의 미해결 문제 10개를 해결하거나 크게 전진시켰다고 발표했다. 발표만 보면 흔한 자화자찬일 수 있다. 이번이 다른 이유는 두 가지 — 기계가 검사한 형식 증명이 공개됐고, 필즈상 수상자가 고개를 끄덕였다.
1. 무엇을 풀었나 — '시험'이 아니라 '미해결'
목록에서 가장 눈에 띄는 결과는 군론(group theory)의 오랜 질문인 비소픽(non-sofic) 군의 존재 증명이다. 수십 년간 '존재할 것 같지만 아무도 증명 못 한' 대상의 존재를 구성적으로 보였다는 주장이다. 구 채우기(sphere packing) — 고차원 공간에 공을 얼마나 빽빽이 담을 수 있는가 — 의 한계 개선, 이진 코드 한계, 산술 회로 복잡도 등도 목록에 올랐다.
핵심 구분은 이것이다. 지금까지 AI의 수학 성적은 올림피아드처럼 '답이 알려진 문제'에서 측정됐다. 미해결 문제는 채점자도 답을 모른다 — 그래서 전진이 사실이라면 이는 지식의 재조합이 아니라 새 지식의 생산이다.
2. 왜 믿을 만한가 — 검증의 세 겹
| 검증 장치 | 내용 | 의미 |
|---|---|---|
| 형식 증명 (Lean) | 증명을 기계 검사 가능한 코드로 작성, 깃허브 공개 | '그럴듯한 오답' 원천 차단 |
| 외부 권위 | 필즈상 수상자 가워스 "최상급 저널에 추천" | 자체 발표 너머의 인정 |
| 공개 검증 | 누구나 증명 코드를 내려받아 검사 가능 | 재현성 확보 |
| 남은 한계 | 10개 전체 목록·구분은 학계 검증 진행 중 | '해결'과 '전진'의 경계 주의 |
| 모델 상태 | 아스트라는 내부 모델, 출시 미정 | 제품이 아니라 능력 시연 |
형식 증명이 이 발표의 기둥이다. Lean 같은 증명 보조기로 쓰인 증명은 컴퓨터가 논리의 모든 단계를 기계적으로 검사한다 — AI의 고질병인 '자신 있는 헛소리'가 통과할 수 없는 관문이다. 형식 증명이 무엇이고 어떻게 작동하는지는 오늘 함께 발행한 기준 문서 「형식 증명이란」에서 뜯어본다.
3. 남은 것
남은 질문은 두 겹이다. 학계 검증이 10개 전부를 인정할 것인가 — '해결'과 '의미 있는 전진' 사이의 경계는 수학자들이 판정할 몫이다. 그리고 이 능력이 수학 밖으로 언제 넘어오는가 — 정답 검증이 수학만큼 깔끔하지 않은 과학·공학에서 같은 일이 벌어질 때, 그 파장은 벤치마크 점수와는 차원이 다르다. AI 능력 경쟁의 다른 축(무료화·오픈모델)은 「챗GPT 무료 무제한」과 「중국 AI 8주 5모델」에서, 검증의 도구는 「형식 증명이란」에서 이어진다.