OpenAI의 양-밀스 증명: Gross 위원회 평가서가 확인한 것과 아직 열려 있는 것

2026년 11월 10일, David Gross가 위원장을 맡은 양-밀스 그룹은 OpenAI가 10월 28일 그룹에 제출한 Lean 코드를, "Validation of the OpenAI Yang–Mills construction"(OpenAI 양-밀스 구성의 타당성 확인)이라는 제목의 35쪽 분량 평가서와 함께 공개했습니다.¹ 평가서 첫머리의 판단은 두 문장입니다. 첫 문장은 그룹이 증명되었다고 보는 내용, 곧 "임의의 콤팩트 단순 게이지 군에 대해, Wightman 공리를 만족하는 상대론적 양자장론을 4차원 Wilson 격자 게이지 이론의 스케일링 극한으로 구성할 수 있다는 것"을 말합니다. 두 번째 문장은 증명되지 않은 것을 말합니다. "이 작업은 무한 부피 극한이 유일하다는 것도, 질량 간극이 있다는 것도 증명하지 않는다."

따라서 밀레니엄 문제는 풀리지 않았고, 평가서도 풀렸다고 말하지 않습니다. 같은 문서는 "우리는 아직 증명을 완전히 이해한다고 주장하지 않는다"고 말하며, 평가가 OpenAI의 별도 비형식적 원고가 아니라 Lean 소스에만 근거한다고 밝힙니다.

아래에서는 무엇이 공개되었는지, 그룹이 무엇은 증명되었고 무엇은 증명되지 않았다고 말하는지, Lean 코드를 어떻게 확인했는지, 그리고 그룹이 스스로의 검토에 두는 한계를 정리합니다. 위원회의 첫 성명은 10월 31일 해설 글 양-밀스 문제와 AI: OpenAI의 주장, Gross 위원회, 공개된 Claude 시도에서, OpenAI의 발표는 10월 27일 해설 글 OpenAI의 카케야, ETH, 양-밀스 주장: 무엇을 말하고 무엇이 아직 열려 있나에서 다뤘습니다. 모든 출처는 2026년 11월 11일에 확인했습니다. 평가서는 그룹 자체의 것이며, 어떤 학술지도 이를 심사하지 않았습니다.

양-밀스 그룹은 11월 10일 무엇을 공개했나요?#

공개 GitHub 저장소 두 개입니다. 위원회는 하루 앞서 세 번째 성명에서 이를 예고했습니다.⁵ 11월 3일의 두 번째 성명은 확인 작업에 대해 "이 작업은 잘 진행되고 있다"고 했습니다.⁶

• yang-mills-group/OpenAI-YM-20261028³ 저장소에는 OpenAI가 10월 28일에 제출한 그대로의 Lean 소스가 있습니다. 이 저장소의 README는 정리와 그 재빌드 방법에 대한 OpenAI 자신의 설명입니다.
• yang-mills-group/YM² 저장소에는 평가서, 제출물을 바이트 단위까지 그대로 옮긴 사본, 그룹 자체의 Lean 확인, 날짜가 적힌 빌드 및 검증 기록, 그리고 이를 다시 실행하는 방법이 있습니다.

세 번째 성명은 평가서를 "이 제출물에 대한 결과와 우리의 확인, 특히 이 제출물이 물리학과 수학에서 표준인 문제 진술에 따라 순수 양-밀스 이론의 존재를 증명한다는 점을 요약한" 문서라고 설명합니다. 성명은 11월 2일 그룹에 합류한 Ron Nissim과 Fred Rajasekaran에게 감사를 전합니다.¹⁰

이번 공개는 Lean 코드만 다룹니다. 위원회의 첫 성명은 모델이 만든 증명이 1,147쪽에 이르며, "증명의 품질과 정확성에 만족하면" 그룹의 평가와 함께 공개하겠다고 했습니다.⁷ 그 비형식적 원고는 두 저장소 어디에도 없고, 평가서는 스스로에 대해 이렇게 말합니다. "이 평가는 별도의 비형식적 증명 원고에 기대지 않는다."

YM 저장소는 11월 4일 자 두 번째 OpenAI 제출물을 "진행 중인 작업"으로 올려 두고 있습니다.²

평가서는 OpenAI의 제출물이 무엇을 증명한다고 말하나요?#

구성은 양-밀스 이론을 격자 위에 올리는 표준 방법인 Wilson의 격자 게이지 이론에서 출발합니다. 평가서는 세 단계를 설명합니다.¹

이어 그룹은 이렇게 만든 대상이 다른 무엇이 아니라 양-밀스 이론인지를 묻습니다. 그룹은 "격자에서 비롯되었다는 점, 국소 장, 정규화된 응력 텐서, 주도적인 단거리 법칙, 연산자 곱 전개"를 들며, 이것들이 "이 구성이 양-밀스 이론을 기술한다는 상당한 증거를 제공한다"고 말합니다. 그 결과 가운데 하나는 응력 텐서 대각합(trace)의 2점 함수인데, 그 주도적인 단거리 계수는 "섭동론적 예측과 일치한다".

평가서는 이 결과를, 자신이 읽기로 Jaffe와 Witten이 쓴 클레이 문제 설명¹¹이 구성된 이론에 요구하는 네 가지 특징과 비교합니다.¹

평가서는 무엇이 증명되지 않았다고 말하나요?#

평가서 첫 페이지는 빈틈 세 가지를 꼽습니다. "질량 간극은 주장하지 않는다. 부피 부분수열들에 걸친 유일성과 성분 이론들의 일치도 해결되지 않았다."¹

두 번째와 세 번째가 중요한 것은 2단계 때문입니다. 증명이 보여 주는 범위에서는 부피의 다른 부분수열이 다른 극한을 줄 수도 있고, 한 극한 안의 성분 이론들이 같은 이론이라는 것도 증명되지 않았습니다. 그룹은 Jaffe와 Witten의 정식화가 "추가 논증이 극한에 필요한 성질을 확립하지 않는 한, 콤팩트성으로 얻은 부분수열 극한을 불충분한 것으로 본다"고 쓰고, 재구성 정리와 국소 장 정리가 "콤팩트성을 넘어서는 상당한 정보를 제공한다"고 씁니다. 그룹은 자신의 기준도 밝힙니다. "여기서 채택한 존재성 기준에서는 진공 상태의 정밀한 특성화를 요구하지 않는다." 그리고 유일성이 빠져 있다는 것이 "무한 부피 극한과 참된 양-밀스 진공이 유일하리라는 일반적인 예상과 모순되지 않는다"고 덧붙입니다.

평가서 8절은 이 작업이 다루지 않는 것을 나열합니다.

• 수렴하는 부분수열만이 아닌 수렴 자체, 그리고 무한 부피 극한의 유일성
• 연속체 이론의 확률 측도
• "균일한 질량 간극"
• Wilson 루프 관측량과, 가둠을 진술하는 통상적인 방식인 면적 법칙
• 단일 입자 상태와 그 에너지-운동량 스펙트럼

본문에는 한계가 두 가지 더 나옵니다. "모든 차수에서의 섭동론적 일치는 증명되지 않은 채로 남아 있다"는 것, 그리고 자유장 기술을 배제하는 정리가 "가우스 장의 합성으로 이루어진 기술을 모두 배제하지는 않는다"는 것입니다.

OpenAI 자신의 README도 같은 선을 긋습니다. "양의 질량 간극, 연속 질량 일반화 자유장의 일반적 배제, 모든 차수의 MS-bar 일치는 범위 밖이다."³

Lean 증명은 어떻게 확인했나요?#

평가서는 두 질문을 구분합니다.¹ 검증(verification)은 증명이 그 정의와 허용된 공리로부터 따라 나오는지를 묻고, Lean 커널이 여기에 기계적으로 답합니다. 타당성 확인(validation)은 그 정의가 물리학자와 수학자가 양-밀스 이론이라고 부르는 것을 말하는지를 묻습니다. 이 질문에는 어떤 커널도 답할 수 없습니다.

재빌드. Lean 4.32.0으로 처음부터 새로 한 빌드(clean build)는 프로젝트 모듈 9,470개를 약 184분 만에 오류 하나 없이 다시 빌드했습니다. Lean 소스 파일 9,477개가 모두 제출물의 매니페스트와 일치했습니다. 프로젝트 선언 250,319개를 전수 조사한 결과, 해답에서 추가된 공리도, Lean의 자리표시 공리(placeholder axiom) 사용도 발견되지 않았습니다. 주요 증명은 표준 공리 세 개, propext, Classical.choice, Quot.sound만 씁니다.

Comparator. Lean에서는 저자가 정리의 대상이 되는 객체를 직접 정의할 수 있으므로, 증명이 통과하면서도 슬그머니 다른 것을 증명하고 있을 수 있습니다. 평가서는 이렇게 표현합니다. "제출된 형식화 작업은 검증 과정에서 문제 진술이나 그 바탕이 되는 정의 하나를 바꿔, 잘못된 증명이 검증되는 것처럼 보이게 할 수 있다." Comparator는 해답을 별도로 고정해 둔 기준 명제와 대조하는 도구입니다. Comparator는 10월 30일 OpenAI의 공개 정리에 대해, 11월 3일 그룹 자체의 통합 정리에 대해, 11월 5일 연산자 곱 전개에 관한 별도 명제에 대해 통과했습니다. 대조 시험 네 가지도 예상대로 작동했습니다. 올바른 증명은 받아들여졌고, 명제를 바꾼 경우, 금지된 공리를 쓴 경우, 정의를 바꾼 경우는 각각 거부되었습니다.

그룹 자체의 Lean 확인. 그룹은 A1에서 A8까지 이름 붙인 독립적인 어댑터(adapter)를 작성해, 구성된 객체가 다른 곳에서 진술된 요구 사항을 충족함을 증명했습니다. 그중 둘은 제출물을 그 밖에서 만든 형식화와 비교합니다. 하나는 이전 프로젝트의 Osterwalder–Schrader 공리로, 그룹은 이것이 "OpenAI의 양-밀스 구성을 알기 전에 독립적으로" 정식화되었다고 말합니다. 다른 하나는 별도의 격자 게이지 이론 저장소에 있는 유한 Wilson 격자 분포(law)입니다. 저장소의 범위 문서는 각 어댑터가 무엇을 다루는지 정확히 밝힙니다. 예를 들어 Osterwalder–Schrader 연결(bridge)은 "그 스칼라 족에 관한 것이지, 별도로 지정된 모든 장에 대한 OS 인터페이스에 관한 것이 아니며", 여기에 쓰인 해석적 추정은 OpenAI의 증명에서 옵니다.⁴

사람의 검토. 그룹은 "Lean 정의에 대한 광범위한(그러나 빠짐없지는 않은) 사람의 검토"를 했다고 보고합니다.

한 가지 발견은 OpenAI 자신이 내세운 대표 정리에 관한 것입니다. 평가서에 따르면 OpenAI는 제출 후 그룹에, 자신의 공개 Comparator 대상인 YangMills.jointExistence가 "그 증명이 확립한, 격자 구성과의 연결 일부를 빠뜨렸다"고 알렸습니다. 그룹의 통합 대상은 그 연결을 유지하고 있으며, 평가서는 그룹의 평가가 "따라서 공개된 존재성 명제만이 아니라 그 더 강한 대상과 아래에 설명하는 확인들에 근거한다"고 말합니다.

그룹은 스스로의 검토에 어떤 한계를 두나요?#

평가서는 그 한계를 숨기지 않고 밝힙니다.¹

• 이해. "제공된 Lean 코드를 소화하는 데 OpenAI의 Astra의 도움을 받았다. 우리는 아직 증명을 완전히 이해한다고 주장하지 않는다."
• 근거 자료. Lean 코드만 평가했습니다. 비형식적 원고는 쓰지 않았습니다.
• 공로 표시. "OpenAI의 작업은 많은 물리학자와 수학자의 선행 연구에 기대고 있다. 공로를 신중히 밝힌 전체 검토는 이후 공개에서 제공할 것이다".
• 격리. Comparator 실행은 macOS에서 개발용 실행기(launcher)로 이루어졌으므로 "잠재적으로 악의적인 빌드 코드의 격리는 시험하지 않는다". 평가서는 이렇게 덧붙입니다. "추가적인 외부 커널 구현은 사용하지 않았다."
• 코드 품질. 그룹은 "Lean 저장소의 코드 품질에 대한 몇 가지 우려"를 표합니다. 선언 250,319개 가운데 주요 정리에 쓰이는 것은 100,168개이며, 그룹은 "선언과 파일에 관례에서 벗어난 이름을 붙였다"는 점을 지적하면서 Kitchen.lean이라는 파일 안의 Cake, cookie 같은 예를 듭니다.
• 독립성. "우리 그룹과 OpenAI의 유일한 연결은 (제출물을 받는 것 외에는) 분석을 돕는 데 그들의 Astra 모델을 쓴 것이다. 우리 그룹은 현재 클레이 수학연구소와 아무런 관계가 없다."

저장소의 제출 정책에는 앞으로의 공개만큼이나 이번 공개에도 해당하는 문장이 있습니다. "제출물을 게시하는 것은 그 주장을 지지하거나 인증하는 것이 아니다."² 그룹의 규정은 평가에 "증명이 옳은지에 대한 우리의 판단"이 들어갈 것이며, 그룹은 "AI 모델이 만들어 낸 발견에 대해 학문적 공로를 구하지 않는다"고 말합니다.⁸

양-밀스 밀레니엄 문제는 풀렸나요?#

아닙니다. 문제는 존재성과 질량 간극을 묻는데, 평가서는 이 구성이 "Jaffe–Witten 문제 전체를 인증하지는 않는다"고 말합니다.¹ 그룹은 또 상을 수여하는 클레이 수학연구소와 현재 아무런 관계가 없다고 밝힙니다. Papex의 양-밀스 존재성과 질량 간극(영어) 페이지에서 이 문제는 여전히 미해결로 올라 있고, OpenAI의 작업은 부분적 주장으로 표시되어 있습니다.

일부 초기 보도는 이번 공개를 증명이 검증되었다는 말로 요약했습니다. 더 정확한 요약은 네 부분으로 이루어집니다.

1. 원로 물리학자와 수학자 다섯 명에 구성원 두 명이 더해진 그룹이, Lean 제출물이 명시된 존재성 기준 아래에서 양-밀스 양자장론의 존재를 증명한다고 판단합니다.
2. Lean 커널, Comparator, 그룹 자체의 어댑터를 통과했고, 누구나 저장소에서 이를 다시 실행할 수 있습니다.
3. 무한 부피 극한의 유일성, 질량 간극, 가둠, 모든 차수의 섭동론적 일치는 증명되지 않았습니다.
4. 그룹은 아직 증명을 완전히 이해한다고 주장하지 않으며, 비형식적 원고는 여전히 공개되지 않았습니다.

첫 성명과 공개 사이에 무슨 일이 있었나요?#

다음에는 무엇이 일어나나요?#

그룹은 아직 남은 일을 밝혀 두었습니다. "공로를 신중히 밝힌" 전체 검토, 11월 4일 제출물에 대한 평가, 그리고 비형식적 증명에 대한 그룹의 해석입니다. 범위 문서는 11월 제출물의 "추가적인 섭동론적 일치 주장"이 이번 첫 패키지의 범위 밖이라고 말합니다.⁴ 저장소는 QCD와 카이랄 SU(5) 게이지 이론에 관한 것을 포함해 추가 제출 제안을 받지만, 이를 게시하거나 검토하겠다고 약속하지는 않습니다.²

다른 독자들에게 이번 공개는 할 수 있는 일을 바꿉니다. Lean 코드가 공개되었으므로, 재빌드와 Comparator 실행을 프로세스 격리를 갖춘 Linux에서, 그리고 두 번째 커널로 반복할 수 있습니다. 그룹의 기준 명제도 공개되어 있으므로, 전문가들은 정의를 읽고 그것이 올바른 정의라는 데 동의하는지 말할 수 있습니다. 형식적 명제가 비형식적 명제와 같은 뜻인지라는 바로 그 질문이, 그룹 스스로 사람의 검토가 아직 필요하다고 말하는 지점입니다.⁴

열린 질문#

• 무한 부피 극한은 부분수열에 따라 달라질까요, 그리고 성분 이론들은 서로 같을까요?
• 1,147쪽 분량의 비형식적 원고는 공개될까요? 공개된다면 언제일까요?
• 11월 4일 제출물은 무엇을 더하며, 그룹의 두 번째 평가는 그 섭동론적 일치 주장을 받아들일까요?
• 독립적인 팀이 Linux 격리와 외부 커널로 확인을 다시 실행할까요?
• 클레이 수학연구소는 문제의 절반인 존재성에 대해 무언가 말할까요?

출처#

1. Validation of the OpenAI Yang–Mills construction: Assessment 1 (양-밀스 그룹, 2026년 11월 10일, 35쪽), 2026년 11월 11일 확인 ↩ a b c d e f g
2. yang-mills-group/YM: README, 제출물, 검증 기록 (GitHub), 2026년 11월 11일 확인 ↩ a b c d
3. yang-mills-group/OpenAI-YM-20261028: OpenAI의 2026년 10월 28일 Lean 제출물과 그 README (GitHub), 2026년 11월 11일 확인 ↩ a b
4. What the formal checks cover (yang-mills-group/YM, submissions/openai-20261028/docs/checks.md), 2026년 11월 11일 확인 ↩ a b c
5. Proof by OpenAI of the existence of Quantum Yang-Mills Theory: 3rd Statement by the Shepherding Committee (2026년 11월 9일), 2026년 11월 11일 확인 ↩
6. Proof by OpenAI of the existence of Quantum Yang-Mills Theory: 2nd Statement by the Shepherding Committee (2026년 11월 3일), 2026년 11월 11일 확인 ↩
7. Proof by OpenAI of the Existence of Quantum Yang-Mills theory: Statement by the shepherding committee (2026년 10월), 2026년 11월 11일 확인 ↩
8. Rules and Procedures of the Yang Mills Group (KITP, 날짜 없음), 2026년 11월 11일 확인 ↩
9. Statement by the Yang-Mills Working Group, 11월 3일과 9일 업데이트 포함 (KITP), 2026년 11월 11일 확인
10. Members of the Yang–Mills group (yang-mills-group/.github, 2026년 11월 8일 갱신된 기록), 2026년 11월 11일 확인 ↩
11. Jaffe, Witten, Quantum Yang–Mills Theory (클레이 수학연구소), 2026년 11월 11일 확인 ↩