AIの「解は一意」を点検する：存在と「高々一つ」を分けよう

AIによる証明案の論理チェック手法。解の「存在」と「一意性」を混同しないための読み解き方として、実数方程式を例に数学的な証明の不備を見抜くポイントをLean 4を交えて解説。