[기사 톺아보기]
AI가 5일 만에 끝낸 필즈상 증명, 진짜 사건은 무엇인가

무슨 일

AI 스타트업 매스(Math Inc.)의 시스템 '가우스'가, 필즈상 수상자 연구팀이 2년 넘게 진행하던 수학 증명 '형식화'를 5일 만에 완료

누구의 증명

2022년 필즈상 수상자 마리나 비아조우스카(EPFL 교수)의 8차원, 24차원 구 채우기 증명

언제

2026년 2월 발표, 24차원은 약 2주 만에 완료

수학계 반응

발전 속도에 놀라면서도, 사람이 직접 증명을 따라가며 배우는 과정의 가치를 강조

함께 거론된 사건

2026년 5월, OpenAI 내부 모델이 80년 묵은 에르되시 '단위 거리' 추측의 반례를 발견

형식화 (Formalization)

사람이 쓴 수학 증명을, 컴퓨터가 한 줄씩 논리적으로 검증할 수 있는 코드로 옮기는 작업입니다. 빠진 가정이나 숨은 오류를 잡아낼 수 있습니다.

증명 보조기 (Proof Assistant)

증명이 빈틈없이 옳은지 컴퓨터가 검사해 주는 프로그램입니다. 이번 작업에 쓰인 것은 'Lean(린)'입니다.

매스립 (Mathlib)

Lean으로 검증된 수학 정리들을 모아 둔 공개 도서관입니다. 누구나 가져다 쓰고, 새 결과를 보태는 공동 자산입니다.

구 채우기 문제

똑같은 공을 빈틈없이 가장 촘촘하게 쌓는 방법을 묻는 문제입니다. 차원마다 정답이 다릅니다.

차원 (Dimension)

방향의 수입니다. 우리가 사는 공간은 3차원입니다. 8차원, 24차원은 수학에서 다루는 더 높은 차원의 공간입니다.

필즈상

4년마다 수여되는 수학 최고 영예입니다. 흔히 '수학계의 노벨상'으로 불립니다.

추측 (Conjecture)

참이라고 강하게 믿지만 아직 증명되지 않은 명제입니다. 증명되면 '정리'가 됩니다.

반례 (Counterexample)

어떤 추측이 틀렸음을 보여 주는 단 하나의 예입니다. 반례가 나오면 추측은 무너집니다.

단위 거리 '문제'는 여전히 미해결

OpenAI가 한 것은 '추측의 상한이 틀렸음'을 보인 반증입니다. 점들이 격자보다 더 촘촘히 1만큼 떨어질 수 있음을 보였을 뿐, 최댓값이 얼마인지는 여전히 모릅니다.

'자율·원샷'이라는 표현의 논란

'한 번에 스스로 풀었다'는 홍보 표현 뒤에는, 연구진이 수개월간 프롬프트와 설정을 다듬은 사전 작업이 있었습니다. 일부 전문가는 '진짜 자율'인지 의문을 제기합니다.

작년의 과장 전례

앞서 한 차례, AI가 여러 에르되시 문제를 '풀었다'는 발표가 사실상 기존 문헌의 재발견에 가까웠던 일이 있었습니다. 이 분야는 과장 경계가 필요합니다.

OpenAI만의 일이 아님

Anthropic도 같은 추측을 자사 시스템으로 반증했다고 보고했습니다. 이후 사람 수학자들이 이에 자극받아 또 다른 추측(에르되시–세메레디)을 반증했습니다.

저명 수학자의 검증

단위 거리 결과는 팀 가워스, 노가 알론 등 최고 수준 수학자가 해설 논문에 참여해 신뢰를 더했습니다. 다만 정식 동료심사는 별개 과제로 남아 있습니다.

가우스가 원증명의 오류를 잡음

형식화 과정에서 가우스는 8차원 원증명의 부호 오류와 '마법 함수' 표현 오류를, 24차원에서는 불완전한 단계를 찾아 고쳤습니다. 형식화가 단순 노동이 아니라 엄밀성을 높임을 보여 줍니다.

'원본 그대로'는 아님

형식화 대상은 비아조우스카의 원증명이 아니라, 약간 수정된 '설계도(청사진)'였습니다. 가우스 코드가 의도한 증명과 정확히 일치하는지는 아직 확인 중입니다.

코드 규모

전체 형식화는 한때 약 50만 줄에 달했고, 정리 후 약 18만 줄로 줄었습니다. '증명을 만드는 일'보다 '깔끔하고 재사용 가능한 코드로 만드는 일'이 더 어려웠습니다.

자금 출처

가우스 개발은 미국 국방고등연구계획국(DARPA)의 수학 프로그램 등에서 지원받았습니다. 'AI 수학'의 배후에 어떤 자본과 목적이 있는지도 함께 보아야 합니다.

논문 1

비아조우스카 (2017), '8차원 구 채우기 문제', Annals of Mathematics. E8 격자가 8차원에서 가장 촘촘한 배열임을 모듈러 형식으로 증명. (arXiv:1603.04246)

논문 2

콘·쿠마르·밀러·라드첸코·비아조우스카 (2017), '24차원 구 채우기 문제', Annals of Mathematics. 리치(Leech) 격자가 24차원 최적임을 증명. (arXiv:1603.06518)

논문 3

하리하란 외 (2026), '8차원 구 채우기 형식화의 진전', arXiv:2604.23468. 이번 사건의 1차 자료. 가우스가 어떤 정리를 어떻게 형식화했는지, 사람과 AI의 협업이 어떠했는지 기록.

구 채우기는 '순수 수학'만이 아님

구 채우기 이론은 '오류 정정 부호'와 직접 닿아 있습니다. 휴대전화, 인터넷, 저장장치에서 잡음이 섞여도 데이터를 복원하는 기술의 수학적 토대입니다.

서로 먼 분야를 잇는 능력

에르되시 반례의 진짜 충격은 'AI가 풀었다'가 아니라, 기하 문제를 전혀 다른 분야인 '대수적 정수론'과 연결해 풀었다는 점입니다. 두 분야를 모두 잘 아는 사람도 드뭅니다.

'검증'과 '발견'은 다른 일

형식화(가우스)는 이미 있는 증명을 '검증'한 일입니다. 단위 거리 반례(OpenAI)는 새 결과를 '발견'한 일입니다. 둘은 난도와 의미가 다른데, 기사는 이를 뚜렷이 구분하지 않았습니다.

1611년

케플러, 3차원 구 채우기 추측 제기

1946년

에르되시, 단위 거리 문제 제기

1998·2005년

헤일스, 3차원 케플러 추측 컴퓨터 보조 증명

2016·2022년

비아조우스카, 8·24차원 구 채우기 해결, 필즈상 수상

2014년

3차원 케플러 추측의 형식 검증 완료 (십수 년 소요)

2026년

AI 가우스, 8·24차원 형식화를 며칠 만에 완료. 금세기 필즈상 업적의 첫 형식화.

증명 신뢰도 향상

사람 손으로 검증 불가능했던 거대 증명도 기계가 확인할 수 있습니다. 수학의 토대가 더 단단해집니다.

연구 가속

지루한 검증을 AI가 맡으면, 사람은 새로운 아이디어와 발견에 더 집중할 수 있습니다.

공동 자산 축적

검증된 정리가 매스립에 쌓이면, 전 세계 연구자가 함께 쓰는 신뢰 가능한 지식 도서관이 커집니다.

응용 분야 확장

구 채우기는 통신·암호·데이터 저장과 닿아 있습니다. 이 토대가 탄탄해지면 응용 기술도 함께 발전합니다.

정확성 (신문윤리강령)

대체로 양호. 다만 '케플러 추측'과 '구 채우기 문제'를 혼용해 부정확. 보완이 필요합니다.

균형·객관성

양호. 복수의 전문가를 인용하고, 기대와 우려를 함께 담았습니다.

맥락 제공

미흡. '자율·원샷' 논란, 작년 과장 전례, Anthropic의 동일 결과 등 중요한 맥락이 빠졌습니다.

과장 경계

양호. 제목이 '문제 해결보다 과정'을 강조해, 성과를 과장하지 않으려 한 태도가 보입니다.

출처 표기

양호. 참고자료로 arXiv 논문과 OpenAI 발표를 명시했습니다.