本研究では，勝敗構造が既知である約数ニムを逆形にしたゲーム（一山の逆形約数ニム）を解析した．逆形約数ニムは，山にある石の個数の真の約数個だけ石を取り除くゲームであり，石の個数を素数にした着手者が敗者となる．石の個数が10^7以下の局面をシミュレーションし，各局面が先手必勝か後手必勝か（必勝戦略保持者）を調査した．その結果と素因数の構造から局面を27通りのパターンに分類し，各パターンの必勝戦略保持者を予想した．石の個数が任意の局面において，この予想が成立することを示すために，生成AIを活用し，証明の自動化を試みた．この生成された証明を分析し，この証明方法の有用性や妥当性について考察した．