Logvinovich, Lean 4로 양밀스 질량 간극 불가능성 주장…표준 구성 틀에 한정
Victor Logvinovich의 RoundSquare는 E(λ)=1/(λ+1) 수열에 양의 하한이 없다는 산술을 Lean 4로 형식화하고, 이를 R⁴ 양밀스 질량 간극 불가능성으로 해석합니다. 저자는 주장의 범위를 표준 구성 틀로 한정하며, 수열과 실제 양밀스 해밀토니안 스펙트럼의 연결은 별개의 물리적 주장입니다. OpenAI가 별도로 발표한 양밀스 존재 증명의 AI 산출물은 연구 그룹의 원고 작성 동안 공개 보류됐습니다.