14/09/07 13:30:56.67
すれ主さん 各種情報提供ありがとうございます。
他の数式処理ソフトで係数を決めた場合の可解性をチェックするソフト検索ありがとうございます。
GAP以外でもできて、しかも比較的ソースが短かいので参考になりそうです。
探してたのは一般的な5次方程式の証明するソースなのです。
> the Odd Order Theoremはこれか？ 有名なFeit?Thompson theorem
その証明のチェックを行なった証明補助ソフトのソースらしきものはありました。
中身みてないけど。
具体的な例じゃなく。一般的な証明そのものを代行あるいは補助してくれるソフトが存在してます。
定理の証明を補助あるいは自動証明するソフトがあるのです。
それらのソフト群のなかで、5次方程式の不可解性の証明(使う演算を制限。みんなわかってるし書く必要ないと思うけど。)を行なうソースを探したけど
ぴったりのものはなかったってことです。
いまや数学の定理の証明も自動化(全部じゃないけど、一部だけ)できるところまできてますよ。
GAPはどうも一般的なものじゃなく具体的なものしか扱えない可能性があります。
ちゃんと使い方確認してないのでわかりませんが。
使ったことあるのは自動証明がそれほど充実してない、補助的なソフトを使ったことあります。
そのなかの一つで the Odd Order Theorem の証明が行なわれたようです。
チェックになってたのでちゃんとした証明なのか、中身を確認してないのでわからない。
特定の数式の証明じゃなく。一般的で私がもともと勉強して理解しようとしてたことを
できて、任意の数学的演算を追加して、それで可解になるかどうかの判定が可能なものが
あるのが理想なのです。
私も検索キーワード工夫して調べてみます。