Hopf 문제의 해결: 6차원 구가 복소다양체 구조를 가짐을 Lean으로 형식화
Formalization of the Solution to the Hopf Problem
6차원 구(6-sphere)가 표준 위상과 호환되는 복소다양체 구조를 가진다는 Hopf 문제의 해결이 Lean 증명 보조기로 형식화되었습니다. 이 저장소는 Levent Alpöge의 논문에 기반하며, Google DeepMind의 Formal Conjectures 프로젝트에서 적응된 명제를 포함합니다. 형식화는 컴퓨터로 검증 가능한 수학 증명의 새로운 이정표를 제시합니다.
6차원 구는 표준 위상과 호환되는 복소다양체 구조를 허용합니다.