Lean으로 확인된 Mochizuki ABC 추측 증명의 공백

Gap in Mochizuki's proof of ABC confirmed by Lean

2026년 7월 17일, ZEN Mathematics Center(ZMC)의 LANA 프로젝트는 기자회견을 열고, IUT 이론의 핵심 논증(Theorem 3.11에서 Corollary 3.12로의 이행)이 형식화 불가능(unformalizable)하다는 결론을 발표했습니다. 이는 2년간의 노력 끝에 나온 결과로, Mochizuki의 설명이 최근 진화하고 있어 최종 판단은 유보했습니다. LANA는 또한 2018년 Scholze-Stix 보고서와의 비교를 포함한 분석 보고서를 공개했으며, 이는 외부 연구자들이 작성한 IUT 이론의 핵심 논증에 대한 관리 가능한 길이의 분석을 제공합니다.