今回は新しい定理を提案してくれるようなプログラムを考えてみました.実際に部分的に作ってみました.そこでなんだかよくわからない結果を得られたので投棄しておきます.(今回の内容はトンデモ成分が多めです.)
数学の定理は複数の定理を組み合わせることで生成されます.そこでとにかく定理を書き連ねて,それらを二つ以上選んで,新しい定理にならないか検証するというアプローチが考えられます.しかしこの総当たりの方法は時間がかかります.そこで次のような「タグ付け」というアイデアを思いつきました.
定理には前提となる部分と結論になる部分があります.そこで定理を前提と結論の二つの部分に分けます.そしてそれぞれに「キーワード」をタグ付けします.
具体例で説明します.定理はアティーヤ.マクドナルドの可換代数入門から引用しました.
定理6.5:をネーター環とし,
を有限生成
加群とする.このとき
はネーター
加群となる.
前提はがネーター環,
が有限生成
加群という二点です.そこで定理6.5の前提に二つのタグNoetherian,FinitelyGeneratedを付けます.
結論はがネーターであるということです.そこで定理6.5の結論にタグNoetherianを付けます.
具体的にはcsv形式で管理します.
可換代数入門の6章までの定理（めんどくさいのでここまで）にタグ付けをして,そこから有向グラフを作ります.すなわち「キーワード(タグ)」をノード,「定理」をエッジとする有向グラフです.定理6.5の例でいえば二つのノードNoetherian,FinitelyGeneratedからNoetherianに向かって二つの矢印が伸びるようにします.
次に経路探索をします.例えばキーワードFieldからNoetherianに二つの定理を経由して行くようなパスを探索します.つまり前提がFieldの情報を持ち,結論にNoetherianの情報を持つような新しい定理を探求します.もちろんタグ付けは荒いので二つの定理がいつでもうまく合体するわけではありません.
試みにIntegral(要素が整であること)からNoetherianに二つの定理を経由して行くようなパスを探索してみました.するとIntegralからFinitelyGenerated(何かが有限生成であることを表したタグ)を経由してNoetherianに行くようなパスが見つかりました.二つの定理を具体的に見てみると
(IntegralからFinitelyGeneratedに行く定理)
定理5.1を環
の部分環とし,
を
上整な元とする.このとき
は有限生成
加群である.
(FinitelyGeneratedからNoetherianに行く定理)
定理6.5:をネーター環とし,
を有限生成
加群とする.このとき
はネーター
加群である.
となります.そこでこれら二つの定理を組み合わせると(この作業は人間が行う)次のような定理が得られます.
謎の定理:を環
の部分環とし,また
をネーター環とする.
を
上整な元とする.このとき
はネーター
加群である.
こうして謎の定理が得られました.二つの定理を組み合わせることで謎の定理が証明されます.
この謎の定理から次のような定理が得られます.
定理:を有理数体
の有限次拡大体,
をその整数環とする.このとき
はネーター
加群である.
は
に有限個の整の元を添加することで作られます.そこで
がネーター環なので謎の定理から
はネーター
加群になります.
この定理は既知のものです.後から気付いたのですが,実際「可換代数入門」の7章に記述がありました.またほとんどのキーワードではゴミみたいな定理しか得られません.
最初はキーワード検索ができるような定理集が作れないかということから出発しました.つまり前提や結論にキーワードを持つような定理を列挙してくれるようなプログラムを考えていました.
