グレブナー基底と自動証明

グレブナー基底大好きbot @groebner_basis

【前回の復習①】 前回はグレブナー基底の定義をしたぶな！グレブナー基底は 「余りを一意的にするイデアルの基底」 だったぶなね。 「記号の説明」のように、変数がn個ある多項式の集合K[x_1,...,x_n]の多項式f,ｇやイデアルI=<f_1,...,f_s>を考えていくぶな

グレブナー基底大好きbot @groebner_basis

【前回の復習②】 gを{f_1,...,f_s}で割ったとき、つまり g=h_1*f_1+...+h_s*f_s + r と書いた時、この r が余りだったぶなね。 グレブナ基底とはどんな{f_1,...,f_s}の順番で割っても r が常に同じになるf_iの組のことだったぶな

グレブナー基底大好きbot @groebner_basis

【前回の復習③】 ここで、ｒ＝０の時を考えるぶな。この時、 g=h_1*f_1+...+h_s*f_s となっているので、これはイデアルI=<f_1,...,f_s>の元になっているぶなね（Iの定義ぶなっ！）。実は、グレブナ基底の余りの一意性から、この逆も成り立つぶな。

グレブナー基底大好きbot @groebner_basis

【前回の復習④】 つまり、 r = 0 ⇔ g は I の元 が成り立つぶな。 一変数の時と同じことが成り立っているぶなねっ！ つまり、グレブナ基底とは、 「ある多項式 g がイデアルに入っているかどうか余りで判定できる」 とても強力な武器であることが分かったぶな！

グレブナー基底大好きbot @groebner_basis

今日は、この【前回の復習】で書いた最後のことを使って、初等幾何の問題を「自動的に」証明していきたいと思うぶなっ！

グレブナー基底大好きbot @groebner_basis

【グレブナー基底と自動証明①】 次の問題を解くぶな！ 問「三角形ABCのそれぞれの辺の中点をD,E,Fとする。この時、線分AE,BF,CDは一点Mで交わることを示せ」 これは中学校でよく見かける「三角形の重心」の問題だぶなっ！ pic.twitter.com/uaiOCb6XkX

拡大

グレブナー基底大好きbot @groebner_basis

【グレブナー基底と自動証明②】 証明:ポイントは、三角形の「相似」に着目するぶな。線分AEとCDの交点は、相似からAEを2:1に分ける点ぶなね。一方、AEとBFの交点も同様にAEを2:1に分ける点ぶな。よって、どちらも同じ点のことぶな pic.twitter.com/fn4xvd2kW4

拡大

グレブナー基底大好きbot @groebner_basis

【グレブナー基底と自動証明③】 フォロワーのみなさんは解けたぶなか？え？相似に気が付かなかった？この証明だとぶなっしー（の中の人）のような頭の悪い人だと中々思いつかないぶなね。 そこで、未来から来たあのロボットを呼ぶことにするぶなっ！ せーのっ！ ぶなえもーーん！！

グレブナー基底大好きbot @groebner_basis

【グレブナー基底と自動証明④】 ぶなえもん「……………」 ぶなっしー「ねえ、ぶなえもん！この問題解いてよっ！」 ぶなえもん「ニュウリョクガナイトケイサンデキヌ」 ぶなっしー「……………」 というわけで、ぶなえもんに計算をさせてなんとか証明をしたいと思うぶなっ！

グレブナー基底大好きbot @groebner_basis

【グレブナー基底と自動証明⑤】 そこで、さっきの「図形」の問題を、ぶなえもんでも分かる「多項式」の問題に置き換えたいと思うぶなっ！ 例えば、O=(0,0),X=(0,x),Y=(0,y) としたとき、点Xが線分OYの中点であることは、多項式 y-2x=0 に置き換えられるぶなっ

グレブナー基底大好きbot @groebner_basis

【グレブナー基底と自動証明⑥】 他にも、画像のように、「図形の世界」の性質（平行、直交、中点など）は「多項式の世界」の言葉で置き換えられるぶな。こうすれば、コンピュータであるぶなえもんにも理解できそうぶなねっ！ pic.twitter.com/Kv1XGtVe16

拡大

グレブナー基底大好きbot @groebner_basis

【グレブナー基底と自動証明⑦】 三角形の重心の問題に戻るぶな。問題の主張を言い換えると「線分AEと線分CDの交点は線分BF上にある」ということぶな。つまり、点Мに対して「MがAEかつCD上にある⇒MはBF上にある」ことぶな。よって、「仮定⇒結論」の主張が見えるぶな。

グレブナー基底大好きbot @groebner_basis

【グレブナー基底と自動証明⑧】 その「仮定」と「結論」をそれぞれ「多項式」の言葉で書き直すと画像のようになるぶな。つまり、「f_1=f_2=...=f_7=0 ⇒ g=0」が示せれば証明終了だぶなっ！ pic.twitter.com/tlViG4fnUb

拡大

グレブナー基底大好きbot @groebner_basis

【グレブナー基底と自動証明⑨】 では、どういう時に、「f_1=f_2=...=f_7=0 ⇒ g=0」が成り立つぶなか？ 例えば、ある多項式h_1,...,h_7 があって、 g=h_1*f_1+...+h_7*f_7 が成り立っているとき、成立するぶなっ！

グレブナー基底大好きbot @groebner_basis

【グレブナー基底と自動証明⑩】 実際、この時には、「f_1=...=f_7=0⇒g=h_1*0+...+h_7*0=0」が成立するぶなね。 g=h_1*f_1+...+h_7*f_7、つまりg が イデアルI=<f_1,...,f_7>の元であることを確認できればいいぶな

グレブナー基底大好きbot @groebner_basis

【グレブナー基底と自動証明⑪】 ここで、グレブナー基底の登場ぶなあああ！ 「前回の復習」で、グレブナー基底は、多項式gがイデアルIに入ってるかどうか分かる強力なツールであることをみたぶな。 ぶなえもんにお願いして、I=<f_1,..f_7>のグレブナー基底を計算してみるぶなっ！

グレブナー基底大好きbot @groebner_basis

【グレブナー基底と自動証明⑫】 Mathematica や Maple などの計算ソフトでグレブナ基底は計算できるぶな。 I=<3ax_8-1, 2x_6-3x_8, 2x_5-3x_7,-3x_8+2x_4,1-3x_7+2x_3,-3x_8+x_2,-3x_7+1+x_1>

グレブナー基底大好きbot @groebner_basis

【グレブナー基底と自動証明⑬】 実際、計算すると上のようなグレブナー基底が得られたぶな。計算ソフトでは、この基底でgを割る計算ができるぶな。すると、 g=(-2x_7+1)*(-3x_8+x_2)+2x_8*(-3x_7+1+x_1) + 0 が得られて余りr=0が分かった！

グレブナー基底大好きbot @groebner_basis

【グレブナー基底と自動証明⑭】 つまり、 r=0 ⇔ g は I の元 ⇒「f_1=...=f_7=0⇒g=0」 ⇔「仮定⇒結論」 ⇔「MがAEかつCD上にある⇒MはBF上にある」 ⇔「三角形の重心定理」 が言えて、相似を使わずにコンピュータで「自動的」に証明が出来たぶなっ

グレブナー基底大好きbot @groebner_basis

【グレブナー基底と自動証明⑮】 まとめると、相似の着目するという「人間的」な証明を、コンピュータを使って「機械的」に証明することができたぶなっ！「ピタゴラスの定理」などの他の図形の問題も同じように解けることがあるぶなよ！ぶなっしーは「正五角形の作図」が正しいか示してみたぶなよ

グレブナー基底大好きbot @groebner_basis

【グレブナー基底と自動証明⑯】 今度は、少し多項式が多くなっているぶなけど、ちゃんと計算で正しいことが確認できたぶなっ！ pic.twitter.com/kGGcVV9ujO

拡大

グレブナー基底大好きbot @groebner_basis

【グレブナー基底と自動証明⑰】 実は、これをさらに一般化したような手法で「限量記号消去法（QE）」という「問題に任意∀や存在∃の記号、不等式があっても答えが出せる」方法が実用化されてるぶなよ。このQEの計算の基礎にもグレブナー基底が使われているぶなっ！

グレブナー基底大好きbot @groebner_basis

【グレブナー基底と自動証明⑱】 今話題の、国立情報学研究所の「ロボットは東大に入れるか」プロジェクト（東ロボくん）でも、数学の入試問題を解く際にグレブナー基底やQEが使われいるらしいぶなよ。詳しくは、参考文献、URLを参照してほしいぶなっ！

グレブナー基底大好きbot @groebner_basis

【今日のまとめ】 「グレブナー基底とコンピュータを使って、定理が『自動的』に証明できることがある！」 ぶなっ！

グレブナー基底大好きbot @groebner_basis

今回のツイートは、参考文献 togetter.com/li/877168 の [1],[6],[7]を参照し、特に「三角形の重心定理の自動証明」の部分は、[1]の第６章「ロボティクスと幾何の定理の自動証明」を元に書きました。