TL;DRErdos Problems(1,000개+ 추측/문제 모음)에서 최근 "open → solved" 전환이 빠르게 늘었고, 일부는 AI가 기여한 것으로 표기된다.대표 사례로 Erdos Problem #728은 OpenAI GPT-5.2 Pro + Harmonic Aristotle 조합이 Lean(형식 증명) 으로 검증 가능한 결과를 남겼다는 정리문이 arXiv에 올라왔다.핵심은 "말로 그럴듯하게 설명"이 아니라, 증명을 코드로 만들고(Lean4) 기계적으로 검증하는 파이프라인이 현실화됐다는 점이다.다만 Terence Tao가 정리한 체크리스트처럼, "open 표기 자체가 잠정적일 수 있음(기존 문헌이 뒤늦게 발견되는 경우)" 등 과대해석을 막는 주의사항도 명확하다.본문1) 지금 무슨 일이 벌어졌나:..