AI·바이브코딩 기술 트렌드

수학 역사상 가장 거대한 증명을 컴퓨터가 검증하다, 유한 단순군 분류 정리의 Lean 형식화

## 만 쪽이 넘는 증명이 컴퓨터 안으로 수학에는 ‘증명은 끝났는데 처음부터 끝까지 다 읽어본 사람은 거의 없는’ 정리가 있어요. 바로 **유한 단순군 분류 정리(CFSG, Classification of Finite Simple Groups)**예요. 100명이 넘는 수학자가 수십 년 동안 수백 편의 논문으로 쌓아 올린 증명인데, 분량이 흔히 1만 ...