Logvinovich, Lean 4로 양밀스 질량 간극 불가능성 주장…표준 구성 틀에 한정

Victor Logvinovich가 공개한 GitHub 저장소 RoundSquare는 Lean 4 형식화와 함께, 비콤팩트한 순수 R⁴에서 양밀스 질량 간극과 표준 공리 조건이 양립하지 않는다고 주장합니다. README가 산술의 출발점으로 제시한 것은 자연수 λ로 색인한 적외선 모드의 에너지 E(λ)=1/(λ+1)입니다. 모든 λ에서 E(λ) 이상의 값이 되는 양의 유리수 하한 Δ=(p+1)/(q+1)이 있다고 놓으면, λ=q+1일 때 (p+1)(q+2)≤q+1이 됩니다. p≥0이므로 왼쪽은 q+2 이상이고, 이는 성립할 수 없습니다. 따라서 이 수열에는 양의 유리수 하한이 없습니다. 양의 실수 하한이 있다면 그보다 작은 양의 유리수도 하한이 되므로, 같은 모순은 실수 하한에도 적용됩니다.

저장소 README는 RoundSquare.lean에서 sorry와 사용자 정의 axiom 없이 증명을 작성했고, 74개 정리의 #print axioms 검사를 했다고 설명합니다. Lean은 코드에 적힌 정의와 전제에서 형식 명제가 도출되는지를 검사합니다. 이 검산과 E(λ)가 실제 양밀스 이론 해밀토니안의 에너지 스펙트럼을 나타낸다는 주장은 별개입니다.

Clay Mathematics Institute의 문제는 각 콤팩트 단순 게이지 군에 대해 R⁴에서 비자명한 양밀스 양자장이 존재하고 질량 간극 Δ>0을 가지며, Wightman 또는 Osterwalder-Schrader 계열의 공리보다 약하지 않은 성질을 만족하는지 묻습니다. 문제에서 질량 간극은 해밀토니안 H의 스펙트럼에 0과 Δ 사이의 값이 없는 상태를 뜻합니다. 따라서 RoundSquare의 수열 계산을 이 문제에 적용하려면 E(λ)가 해당 이론의 실제 스펙트럼을 나타낸다는 연결이 필요합니다.

Logvinovich의 원고는 불가능성 주장의 범위를 게이지 고정, Faddeev–Popov, Gribov–Zwanziger 지평선, 표준 공리적 양자장론을 포함한 표준 구성 틀로 한정합니다. 아직 발견되지 않은 다른 틀까지 불가능하다는 주장은 정리가 아닌 해석이라고도 명시합니다. 저자는 콤팩트 구성 다양체 M_tot=S⁴×T³에서 질량 간극이 자동으로 생긴다고 주장하지만, 이 결과가 R⁴의 Clay 문제를 푼다고 보지는 않습니다. 원고는 유클리드 공간과 민코프스키 시공간 사이의 연결이 실패한다고 설명합니다.

OpenAI는 2026년 10월 26일 자사 모델이 네 차원 양자장론의 존재 증명을 만들었으며, 그 하위 문제로 순수 양밀스 이론의 존재를 다룬다고 밝혔습니다. 물리학 연구 그룹은 AI 산출물 공개를 보류하고 원고를 작성하기로 했습니다. 이 산출물이 공개되지 않은 상태여서 Logvinovich의 형식화와 OpenAI가 발표한 결과의 세부 증명을 직접 대조할 자료는 현재 공개돼 있지 않습니다.