#증명 소화

[특집] AI가 쓴 증명은 누가 소화하나 — 타오의 '증명 소화불량'과 해설 실측

기계가 증명을 만들고 Lean이 검증까지 끝냈는데, 문제는 여전히 '열림(open)'이다. 아무도 그 증명을 소화하지 못했기 때문이다. 테렌스 타오가 이름 붙인 '증명 소화불량'의 뜻과 역사, 증명을 '이해했다'를 재는 교육학의 일곱 가지 잣대를 살펴본다. 그런 다음 OpenAI가 IMO 2025에 낸 날것의 답안 다섯 편을 AI에게 세 가지 문체로 해설시키고, 원 증명을 보지 못한 '눈먼 독자' 모델에게 읽혀 이해도와 오류 탐지를 직접 쟀다.