>331
おれは将棋のプログラム作ったことあるよ。
　弱いけどね。。。

　結局のところ、探索をどこで打ち切るか？というのは速度の
　問題でもあるが、つきつめれば盤面評価関数を
　どのように作るかの問題なんだ。

　盤面評価関数は、その盤面上の状況に数値を
　あてはめて、得点をつけるわけだ。
　それで得点の高いほうを選択するわけ。

　数学の証明をそのように得点化して評価できるかというと、
　多分、無理じゃないかな？