AI 수학 난제 해결, 성과와 수학자들의 반론

AI가 오래된 수학 문제의 해법을 내놓고, 컴퓨터가 확인할 수 있는 증명까지 붙였습니다. 그런데 수학자들은 왜 반론을 제기할까요? OpenAI의 수학 연구 공개를 둘러싼 논쟁에는 개별 증명의 정확성뿐 아니라, 누가 내용을 이해하고 설명할지, 검토에 드는 일을 누가 책임질지라는 질문이 함께 있습니다.

AI가 만든 결과의 수, 그 결과를 확인한 범위, 수학적 지식으로 받아들이는 과정은 서로 다릅니다. 형식 검증은 중요한 진전입니다. 동시에 공개된 원고와 형식 증명이 어떻게 대응하는지, 새로 발견한 내용은 무엇인지, 연구자가 이어서 활용할 수 있는 설명이 있는지도 살펴야 합니다.

수학자들의 반론도 같은 잣대로 읽어야 합니다. 특정 논증의 불일치를 지적한 연구, 기업의 공개 방식을 비판한 성명, AI를 적극 활용하자는 제안은 발언 주체와 목적이 다릅니다. 이 차이를 따라가면 성과를 인정하면서도 아직 남은 질문을 구체적으로 볼 수 있습니다.

722편의 원고와 난제 해결 수는 다르다

OpenAI는 10월 6일 미공개 내부 모델이 만든 수학 연구 결과를 공개했습니다. 최초 저장소 안내에 적힌 규모는 원고 722편, 관련 결과 묶음 372개입니다. 한 묶음에는 주결과, 이를 받치는 보조 논증, 파생 결과나 다른 증명이 함께 들어갈 수 있습니다. 722라는 숫자를 독립적인 난제 722개를 해결했다는 뜻으로 읽을 수는 없습니다.

공개한 자료에는 원고 외에도 여러 결과의 Lean 형식화와 검사용 설정, 모델 추론의 요약이 포함됩니다. 외부 연구자가 발표 문구만 보는 데서 나아가 실제 산출물을 검토할 수 있게 했다는 점은 의미가 있습니다. 그러나 원고마다 확인 수준이 다르고, 모든 원고에 형식 증명이 붙은 것은 아닙니다.

현재 저장소 안내의 원고 수는 719편입니다. 10월 7일자 변경 이력은 주결과 형식화 비율을 300/719, 약 42%로 보고합니다. 이는 OpenAI가 기록한 형식화 상태입니다. 수학 공동체의 승인율이나 모든 원고의 논증을 외부 전문가가 검토한 비율로 읽으면 안 됩니다.

722편에서 719편이 된 데는 구체적인 이유가 있습니다. 한 대수기하학 원고의 부호 오류로 필요한 항들이 상쇄되지 않으면서 핵심 구성이 무너졌고, 그 구성에 의존한 후속 두 원고도 함께 철회됐습니다. 변경 이력의 표제는 10월 7일이지만 개별 철회 통지는 10월 6일 철회라고 적습니다. 이 통지는 제시한 증명을 철회하는 것이며 수학적 명제가 거짓이라고 주장하는 것은 아니다라고 명시합니다. 증명에 구멍이 생겼다는 판정과 반례를 찾아 명제가 거짓임을 보였다는 판정은 다릅니다.

같은 변경 이력은 별도 14편의 증명 수리, 명제·가정·의존 관계 보정, 오래된 인용 수정도 기록합니다. 그에 따른 추가 13편의 인용 판본·날짜 갱신은 구분해서 적었습니다. 이 숫자들을 모두 새로운 증명 오류나 추가 철회로 합치면 수정의 성격이 달라집니다. 반대로 바뀐 것이 인용뿐이었다고 요약해도 중요한 수리를 놓칩니다.

하나의 구성에 기대던 후속 결과까지 영향을 받은 일은 원고 사이의 의존 관계가 왜 중요한지 보여 줍니다. 공개 자료의 가치는 어떤 주장이 어떤 이유로 바뀌었는지 추적할 수 있다는 데 있습니다. 발표 때의 총량보다 관심 있는 결과의 현재 원고, 형식화 상태와 수정 이유를 함께 읽는 편이 정확합니다.

수학자들은 무엇에 반대했나

공개 전에 나온 자문부터 살펴볼 필요가 있습니다. 수학·AI 자문 그룹 AGMAI는 9월 29일 책임 있는 공개에 관한 권고에서, 연구 공동체가 접근할 수 없는 비공개 모델로 고급 수학 문제를 시험하는 관행을 지지하지 않으며 중단을 요청한다고 밝혔습니다. 단순히 “AI도 틀릴 수 있다”는 주의 문구보다 강한 입장입니다.

동시에 이미 중요한 결과를 얻었다면 책임 있게 신속히 공개하라고 권고합니다. 수학자가 내용을 이해하고 책임지는 원고에는 통상적인 논문 공개·심사 절차를 제시합니다. 사람이 아직 이해하지 못한 AI 결과에는 회사가 먼저 선행연구를 확인하고 읽을 수 있는 증명을 작성하며, 모델·프롬프트·추론 요약·시간·연산비용과 형식화 상태를 밝히도록 요구합니다. 여러 결과를 한꺼번에 냈다면 문제 선택 과정과 비슷한 난도에서 실패한 시도도 공개하도록 합니다. 이해와 설명을 위한 후속 연구 지원도 제안하되, 연구 방향과 지원 배분은 공동체가 독립적으로 결정해야 한다고 봅니다.

쟁점은 증명을 생산하는 능력과 그 결과를 이해 가능한 지식으로 만드는 책임을 함께 부담하는가입니다. 몇 줄의 검사 결과를 제시하는 것과, 다른 연구자의 질문에 답하고 선행연구와의 관계를 설명하는 일은 다릅니다. 수백 편을 공개하면 이 후속 작업의 규모도 커집니다.

더 강한 반대도 있었습니다. Association for Human Mathematics(AHM)의 소통 실무그룹은 10월 6일 공개에 대한 성명에서 700편 이상의 일괄 공개 방식을 비판하고 OpenAI와의 협력 중단을 촉구했습니다. 이 성명은 테렌스 타오의 블로그에 10월 7일 재게시됐지만, 서문과 서명은 단체의 기고임을 밝힙니다. 이를 타오 개인의 성명이나 수학계 전체의 보이콧 선언으로 옮기면 발언 주체가 달라집니다.

자문단과 이 단체도 구분해야 합니다. AGMAI의 10월 6일 성명은 자문이 결과의 영향 평가나 생산 과정의 승인을 뜻하지 않는다고 명시합니다. 공개를 이해의 시작으로 보고 연구자가 기업이 정한 문제 외에 자기 질문을 탐구할 자유와 도구 접근을 강조하면서, OpenAI와의 대화는 건설적이었다고 평가합니다. 두 문서를 하나의 찬성·반대 표시로 합칠 수는 없습니다.

Lean이 검사하는 것은 무엇인가

수학의 명제는 참인지 거짓인지 따질 수 있는 주장입니다. ‘연속한 두 정수의 곱은 짝수다’가 한 예입니다. 몇 가지 숫자에서 계산이 맞는 것을 넘어 모든 해당 경우에 성립하는 이유를 보이는 것이 증명입니다. 두 정수 중 하나가 짝수이므로 그 곱도 짝수라는 논증은 그 이유를 설명합니다.

Lean은 명제와 증명을 엄밀한 형식 언어로 표현하고 확인하는 도구입니다. 형식화를 만드는 사람이나 AI가 자연어의 ‘모든’, ‘어떤 조건에서’, ‘무엇이 성립한다’를 정확한 대상과 가정으로 적습니다. 출발점으로 받아들이는 전제를 공리라고 합니다. 형식 증명이 만들어지면 커널이라는 핵심 검사기가 지정된 정의와 공리 안에서 증명이 유효한지 검사합니다. Lean 공식 검증 안내는 증명의 유효성과 정리 문장의 의미를 구분합니다.

사람이 읽는 증명은 독자가 알고 있을 정의나 중간 단계를 짧게 생략하기도 합니다. 앞의 짝수 설명을 그대로 형식화한다면 첫 정수가 짝수인 경우와 홀수인 경우를 나누는 근거가 필요합니다. 형식화에서는 이런 연결을 검사 가능한 형태로 나타냅니다. 정수를 하나씩 끝없이 대입하는 것이 아니라, 어느 정수를 골라도 적용되는 일반적인 논증을 확인하는 것입니다.

모든 세부를 사람이 매번 처음부터 길게 적어야 하는 것은 아닙니다. 이미 확인된 정리를 가져오거나, 증명을 구성하는 자동화 명령인 전술(tactic)을 사용할 수 있습니다. 작성자가 명령을 짧게 썼더라도 최종적으로 만들어진 형식 증명은 커널의 검사 대상입니다. 핵심은 글의 길이가 아니라, 생략해 보였던 연결에도 확인할 수 있는 근거가 붙었는지입니다.

이 구분을 가상의 주문 확인으로 옮겨 보겠습니다. 주문 A와 B는 발송돼 배송 기록이 있고, 주문 C는 아직 발송하지 않아 기록이 없습니다. 확인하려는 말은 “모든 주문에 배송 기록이 있다”입니다. 이 말은 세 주문 모두를 대상으로 하면 틀립니다.

그런데 이를 “발송한 주문에는 모두 배송 기록이 있다”로 바꾸면 A와 B만 확인해 맞다고 답할 수 있습니다. 좁아진 주장에 대한 검사는 정확해도 원래 주장은 확인되지 않았습니다. 검사 대상에서 빠진 C가 그 차이를 보여 줍니다. 이는 명제의 범위 변경을 설명하는 가상 사례이며, 실제 Lean 실행이나 특정 수학 원고의 재현이 아닙니다.

크게 보기

×확대 이미지 닫기

수학에서는 조건 하나를 추가하는 것이 이런 차이를 만들 수 있습니다. ‘연속한 두 정수의 곱은 짝수’ 대신 ‘첫 정수가 짝수일 때 그 곱은 짝수’를 증명하면 더 좁은 주장입니다. 첫 정수가 홀수인 경우를 다루지 않았기 때문입니다. 검사기가 그 좁은 명제를 올바르게 확인했다고 해서 원래 명제 전체의 증명으로 바로 옮겨갈 수는 없습니다.

형식 검증이 약하다는 뜻은 아닙니다. 원래 대상·가정·결론을 정확히 고정했을 때, 검사 성공은 바로 그 명제에 대한 강한 증거가 됩니다. 그래서 Lean 공동체의 증명 확인 기준은 저장소가 빌드되는지만이 아니라, 실제로 무엇을 증명했는지와 허용한 가정도 확인하도록 합니다. 증명을 생략한 부분이나 허용하지 않은 추가 공리에 기대고 있지 않은지도 확인해야 합니다. 정리의 이름만 원래 난제와 같다고 의미까지 같아지는 것은 아닙니다.

같은 결론을 다른 논증으로 증명한 경우

질문을 정확히 옮겼더라도 남는 구분이 하나 더 있습니다. 형식 증명이 원래 글의 논증과 같은지는 별개의 문제입니다. AI가 글을 옮기다가 오류를 고치고 다른 증명을 찾을 수도 있습니다.

아주 작은 수학 예시를 보겠습니다. “24는 6으로 나누어떨어진다”는 결론은 참입니다. 그런데 누군가 “24는 6×3이므로 그렇다”고 설명했다면 논증에 오류가 있습니다. 6×3은 18입니다. 이 설명을 형식 증명으로 옮기는 AI가 ‘6×4=24’를 사용해 올바른 증명을 만들었다고 가정해 보겠습니다. 그러면 24가 6으로 나누어떨어진다는 명제의 증명은 성립할 수 있습니다. 원래의 ‘6×3’ 설명까지 맞아진 것은 아닙니다.

크게 보기

×확대 이미지 닫기

이 예시는 두 가지 다른 약속을 나눕니다. “이 명제의 올바른 증명을 찾아 주세요”가 요청이었다면 새로운 증명은 성공일 수 있습니다. “이 글의 논증을 그대로 옮겨 오류가 없는지 확인해 주세요”가 요청이었다면, 다른 논증을 찾은 것으로 원문 검토까지 끝냈다고 말하기는 어렵습니다.

증명을 찾는 일과 검사하는 일은 역할도 다릅니다. 어떤 보조 결과를 쓰고 어떻게 연결해야 할지는 사람이나 AI가 탐색할 수 있고, Lean의 자동화가 일부 단계를 도울 수 있습니다. 하지만 검사할 수 있다는 사실만으로 모든 난제의 증명을 찾아 준다는 보장은 없습니다. AI가 만든 후보를 형식화하는 가치는 설득력 있는 문장을 읽는 데서 나아가, 형식 언어로 구성한 논증이 정해진 규칙을 따르는지 확인할 수 있다는 데 있습니다.

반대로 형식 증명이 원문과 다르다는 사실만으로 정리 자체가 틀렸다고 결론 낼 수도 없습니다. 같은 명제에 올바른 증명이 여러 개 있을 수 있습니다. 확인할 것은 명제의 참과 거짓인지, 특정 논증의 정확성인지입니다. 이 차이를 놓치면 유효한 형식 증명을 과소평가하거나, 원래 설명까지 검증됐다고 과대평가하게 됩니다.

나비에–스토크스 논쟁에서 제기한 질문

실제 연구에서 원문과 형식 증명의 차이는 간단한 곱셈보다 훨씬 긴 보조 논증과 가정의 대응에서 생깁니다. 앞의 예시는 무엇을 나눠 확인해야 하는지 보여 주기 위한 것입니다.

이 구분을 실제 AI 수학 원고에 적용한 연구 프리프린트 v1가 10월 6일 공개됐습니다. Alexander Bastounis, Fabian Circelli, Anders C. Hansen은 OpenAI가 9월에 공개한 나비에–스토크스 자연어 증명과 고정 커밋 f9e8bc5의 Lean 형식화가 의미를 충실히 보존하는지 분석했습니다. 나비에–스토크스 방정식은 유체의 움직임을 기술합니다. 이 비판은 앞서 다룬 대수기하학 원고 3편의 철회와 다른 원고를 대상으로 합니다.

한 사례는 출력의 변화량을 입력의 어느 정도 정보로 제한할 수 있는지 나타내는 보조 추정식입니다. 원문 보조정리 8.6은 출력의 m차 미분량 상한을 입력의 m+4차까지의 정보로 제어하지만, 대응하는 Lean 선언은 m+5차 정보까지 사용한다는 지적입니다. 두 쪽 모두 매끄러운 함수를 다루는 상태에서, 출력의 같은 차수 미분량을 제한하는 데 쓰는 입력 정보가 한 단계 더 많아진 것입니다. 저자들이 묻는 것은 원문이 약속한 정도의 정량적 추정까지 형식 증명이 확인했느냐입니다.

비판 저자들은 자연어 증명 자체의 참·거짓을 판정하는 것이 아니라 Lean 번역의 불일치를 분석한다고 명시합니다. 또한 이 보조 추정식의 차이만으로 최상위 나비에–스토크스 정리의 문장까지 다른 문제로 바뀌었다고 결론 낼 수는 없습니다. 원문 논증의 정확성, 중간 결과의 대응, 최상위 형식 명제의 유효성은 나눠 확인해야 합니다.

이 점은 반론에서도 중요합니다. 수학자 Matt Baker는 10월 8일 글에서 자연어 원고의 설명에 틈이 있을 가능성과 Lean으로 정리의 증명을 확보했는지를 구분합니다. 같은 글의 Kevin Buzzard 직접 댓글은 OpenAI가 독립된 Formal Conjectures에서 가져온 최상위 명제가 표준 문제에 대응한다고 강조합니다. 이는 최상위 명제의 의미에 대한 전문가의 평가이며, 원문의 모든 중간 주장과 논증이 같은 형태로 검증됐다는 보증으로 확대할 수는 없습니다.

문제의 범위도 이름만으로 판단하면 안 됩니다. OpenAI의 별도 발표는 외력이 있는 붕괴 사례에 관한 Clay 문제의 C·D 대안을 증명했다고 주장합니다. Clay의 공식 문제 자체에 이 대안이 포함되므로, 외력이 있다는 사실만으로 밀레니엄 문제와 무관하다고 할 수는 없습니다. 어느 방향으로 해석하든 실제 문제 진술과 증명 대상을 확인해야 합니다.

여기서 얻을 수 있는 교훈은 ‘검증됐다’는 설명에 목적어를 붙여야 한다는 것입니다. 원래 논문의 모든 문장을 확인했는지, 같은 정리를 다른 경로로 증명했는지, 보조 결과만 검사했는지에 따라 전달할 수 있는 결론이 달라집니다.

증명의 확인과 발견의 평가는 다른 질문

올바른 증명이 있다는 것과 새로운 수학적 발견이라는 것도 같은 판정은 아닙니다. 이미 알려진 결과를 다시 찾았을 수도 있고, 기존 정리의 새 증명이나 더 좁은 경우의 진전일 수도 있습니다. 각각 의미가 있지만 원래 난제 전체를 해결했다는 말과는 범위가 다릅니다. 선행연구와 문제의 조건을 대조하는 일이 필요합니다.

확인된 형식 증명은 다음 연구에 쓸 수 있는 재료이기도 합니다. 결과 A에서 B가 따라온다는 증명이 있고 A의 증명도 확보했다면, 둘을 연결해 B를 얻을 수 있습니다. Lean에서는 이미 증명된 정리를 이런 방식으로 재사용할 수 있습니다. 다만 이름이 비슷한 정리를 가져오는 것으로 충분하지는 않습니다. 정의와 필요한 가정이 맞아야 하며 새로운 연결도 검사할 수 있게 구성해야 합니다. 새 난제를 해결한 결과가 아니어도 재사용 가능한 증명으로 공개하는 작업에는 이런 가치가 있습니다.

사람의 이해도 별도의 역할을 합니다. 형식 증명으로 참임을 확인할 수 있어도, 어떤 아이디어가 핵심인지 설명하고 다른 문제에 적용하는 데는 추가 작업이 필요할 수 있습니다. 사람이 아직 설명을 충분히 이해하지 못했다는 이유만으로 형식 증명이 틀렸다고 할 수는 없습니다. 정확성을 확인하는 일과 지식을 활용할 수 있게 만드는 일이 다르다는 뜻입니다.

타오 본인은 10월 9일 강연과 이를 소개한 「Math 2.0」에서, 난제 해결 수에 지나치게 집중하는 흐름을 비판합니다. 강연 슬라이드는 난제를 연구 방향을 알려 주는 등대로 보며, 풀어 가는 중에 얻는 통찰과 새로운 질문의 가치를 강조합니다. 동시에 AI를 설명 개선, 논문 사이의 연결, 형식 라이브러리와 가정 변경의 탐색에 활용하자고 제안합니다. 이를 AI 수학 연구 전체를 거부하는 입장으로 요약하면 긍정적인 제안까지 사라집니다.

운영 현장에서 벌어진 일도 있습니다. 수학자 Thomas Bloom은 10월 6일 에르되시 문제 사이트의 변경을 알린 글에서, 설명 없는 AI 증명과 우선권 주장을 올리는 일이 주된 참여 방식이 됐다고 보고했습니다. 거의 모든 새 댓글을 거부해야 하는 조정은 지속하기 어려웠다며 새 문제 댓글·증명 주장 접수를 잠시 멈추고, 해결 상태와 해결률 표시를 없애며 해설에 집중하겠다고 발표했습니다. 이는 AI 활용이 늘던 기간에 대한 운영자의 판단으로, 같은 날 OpenAI가 낸 원고 묶음 하나만을 원인으로 삼은 조치는 아닙니다.

Bloom은 올바른 형식화와 좋은 설명이라면 학계 소속이나 AI 사용 여부와 관계없이 연결하겠다고도 했습니다. 이 사례가 보여 주는 문제는 답의 생산량이 늘었을 때, 질문·토론·설명을 위한 공간을 어떻게 유지하느냐입니다. 수학적 결과의 가치와 참여 방식의 품질을 함께 따져야 한다는 뜻입니다.

공개를 늦추는 것에 반대하는 수학자도 있습니다. Buzzard는 대량 공개 이전인 10월 1일 글에서 기업이 이미 얻은 결과를 연구자가 모른 채 같은 정리를 계속 증명하려 할 수 있으므로 공개를 서둘러야 한다고 주장했습니다. 설명 정리에는 기업의 지원이 도움이 된다고 보면서도, 문제 풀이 능력에 비해 새 이론·추측을 만드는 능력은 증거가 적다고 평가합니다. 이 글은 공개와 이해의 순서에 관한 다른 입장이지, 이후 나온 722편을 읽고 품질을 승인한 평가는 아닙니다.

‘재현할 수 있는가’도 목적어를 붙여 읽어야 합니다. 공개된 형식 증명을 다시 검사하는 일과, 같은 모델·프롬프트·연산 조건으로 증명을 다시 생성하는 일은 다릅니다. 내부 모델이 공개되지 않았다는 점은 생성 과정의 반복에 제약을 주지만, 이미 공개된 Lean 산출물의 재검사가 곧 불가능하다는 뜻은 아닙니다.

OpenAI의 공식 비교 검사 안내는 5개 설정이 해당 원고의 주정리 전체가 아니라 보조 결과를 확인한다고 설명합니다. 따라서 ‘검사 파일이 있다’는 사실에서 멈추지 않고, 그 파일이 어느 주장을 확인하도록 구성됐는지까지 봐야 합니다. 이런 자료가 공개돼 있다는 점은 외부 검토를 가능하게 하는 성과이며, 그 자료의 존재가 모든 검토의 완료를 뜻하지는 않습니다.

난제 해결 뉴스를 읽는 순서

일반 독자가 수백 편의 증명을 직접 검사하기는 어렵습니다. 그렇지만 보도나 발표가 주장하는 범위를 확인하는 일은 할 수 있습니다. 원고 수를 난제 해결 수로 바꿔 말하지 않았는지, ‘형식화가 있다’와 ‘원문 전체가 검증됐다’를 구분하는지, 비판한 수학자의 실제 글이 연결돼 있는지부터 볼 수 있습니다.

1. 원래 문제와 결과전체 해결인지, 특수 경우인지, 보조 결과인지와 원고 수의 단위를 확인합니다.
2. 검사 대상과 가정형식화가 어느 명제를 다루며 원래 조건을 유지하는지 살핍니다.
3. 공개 자료와 현재 버전원고·증명·검사 설정, 개별 철회 통지와 수정 이력을 함께 봅니다.
4. 반론의 주체와 대상개별 증명의 비판인지, 공개 책임이나 연구 방향에 대한 의견인지 원문에서 구분합니다.
5. 확인된 범위로 전달기업의 주장·검사 결과·전문가 평가를 나누고 단체 기고를 개인 성명으로 옮기지 않습니다.

검토가 진행 중인 결과를 전달할 때는 “난제를 풀었다” 대신 “해결을 주장하는 원고를 공개했다”, 확인된 형식 명제가 있다면 “해당 명제의 형식 증명을 공개했다”처럼 근거에 맞춰 말할 수 있습니다. 전문가가 실제로 검토한 대상과 판단을 밝히면 독자는 한 단계 더 구체적인 정보를 얻습니다.

이 원칙을 일상 AI 답변에도 연결할 수는 있지만 검증 방식까지 같아지는 것은 아닙니다. 계산식이 맞아도 집계 대상이 틀리면 업무 답은 틀릴 수 있다는 관계는 비슷합니다. 반면 현실의 영업시간이나 정책은 논리적 증명만으로 확인되지 않습니다. 그런 정보에는 원문과 적용 조건을 확인하는 답변 검토 방법이 필요합니다.

AI가 새로운 증명을 찾고 이를 검사 가능한 자료로 공개하는 것은 수학이 활용할 수 있는 재료를 늘립니다. 그 재료가 널리 쓰이는 지식이 되려면 원래 문제와의 대응, 선행연구와의 관계, 사람이 이해하고 이어서 연구할 수 있는 설명이 함께 필요합니다. 수학자들의 반론은 이 과정의 어느 부분이 부족한지 묻는 질문으로 읽을 때 가장 유용합니다.

그래서 ‘AI가 난제를 풀었다’는 소식 뒤에 덧붙일 정보는 어떤 결과를, 누가 어디까지 검토했고, 무엇을 설명하거나 수정해야 하는가입니다. 검증 가능한 성과를 인정하는 일과 공개·설명의 책임을 요구하는 일은 함께 할 수 있습니다. 해결한 문제의 개수와 반대 의견의 강도만으로는 그 사이의 중요한 차이를 알 수 없습니다.