14/09/07 16:37:03.15
>>289
どうもです スレ主です
了解です。大体考えていることと、レベルが分かったし、すでにレスしたことに含まれていることが多いので簡単に返答します
>探してたのは一般的な5次方程式の証明するソースなのです。
それはおそらく無い。もしあっても、本質はガロア理論だから、コンピュータ証明する余地ほとんどないから
>> the Odd Order Theoremはこれか？ 有名なFeit?Thompson theorem
>その証明のチェックを行なった証明補助ソフトのソースらしきものはありました。
ああ、>>275で”This work was achieved by the team formed by addressees of Georges’ mail, team strongly led by Georges Gonthier.
It is the end of a 6-year long research effort (almost fulltime work) started in May 2006. After the Four Color theorem, this is the second impressive mathematical theorem totally proved in the Coq proof assistant. ”とあるでしょ？
6-year long research effort ＝ 証明はCoqだけでは動かない。だから、補助のプログラムとか数学知識データベースを入れた。それに６年だと
で、5次方程式のガロアは、前処理でほぼ１００％なんだろう。方程式の群論の数学ルールを教える即証明でしょう
the Odd Order Theoremとの違いは下記
URLﾘﾝｸ(homepage3.nifty.com) 五味健作>>276
（抜粋）
有限群論における証明が長く複雑になることが多いのは事実である． それは何故だろうか？
飯高茂先生「しばしば証明は恐ろしく長く，しかも自給自足的である．」
この「自給自足的」ということこそ有限群論の本質であり，証明が長くなる理由ではないだろうか．
全編が，気の遠くなりそうな細かい組み合わせ論法で占められている．
このように，起重機のような大がかりな機械が役に立たないという有限群論の性格は，二三十年たった今でも変わっていないように見える．
（引用おわり）
気の遠くなりそうな細かい組み合わせ論法＝コンピュータ様の得意分野ってことさ。だから、ルールを教えてCoqにかける意味がある
だが、5次方程式のガロアにはそれはないってこと