수학의 아포칼립스

OpenAI가 수학 난제 372건의 성과를 공개했으며, 여기에는 Unique Games Conjecture(UGC)의 증명도 포함됨. 다만 일부에만 Lean 인증서가 있고, 인간이 증명을 이해하는 작업은 이제 막 시작됨
형식적 증명과 인간의 이해 사이의 간극이 핵심 과제로 떠오름. UGC를...