2017-09

目次

≪ 述語論理と全称記号、存在記号 ALL プログラマー ≫

スポンサーサイト

上記の広告は1ヶ月以上更新のないブログに表示されています。
新しい記事を書く事で広告が消せます。

メタ

+βの中ではホンノリとホットな話題であるコンピューターと数学的な証明についての記事を書きたいと思った。一晩記事を書く前に考えてみた。これが結構難しい。自分の意見がまとまらない。感情的には立場は決まっているのだが、論理を少しばかり付けたいと考えてみると自分の中でさえ決定的な所にたどりつかない。そんなもん人様が読む記事に書いてどうするんだ、そう思いつつ、それでも何か言いたい。そういったしだいで結論のない文章だがブログに掲載する。 コンピュータを使った証明として次の二つがあると思う。

(1)証明又はその一部において膨大だが有限なパターンを尽くすためにコンピューターを使って調べつくす。

(2)論理の飛躍を避けるために数学証明をプログラミング言語に翻訳する。またはコンピューターによる論理チェッカーを使用して証明とする。

(1)は問題ないと思う。というか物理学科出身の私としては現実主義であるから「単純作業だが膨大なパターン」と聞いたらそれはコンピューターの出番だと思うのだ。問題にしたいの(2)である。


コンピューターを使った証明、特に証明のプロセスをチェックできない程膨大なプログラムを数学的な証明として(心情的に)受け入れられるか? と言う事だ。(この問題は(1)の場合にも起こりえるが、取り合えず短いプログラムで変数を回すだけという事を念頭に置いている。pentiumにバグがあったりしたろとかを考えると気が狂いそうである)

膨大であろうが証明は証明であろうが、それを受け入れるかどうか。極端な話プログラムが部屋を埋め尽くすような長さになったとして、プログラムの製作者以外に誰もチェックできないとしよう。これは証明として認められるか? 証明のプログラムをチェックするのはプルーフ・チェッカーというものが使われるそうである。プログラムをチェックするメタプログラムか、素人目にはプルーフ・チェッカーは大丈夫なのだろうかと思ってしまう(誰かおしえてくれー)。そんな事を考えていたらメタはそのメタ、またそのメタと数学的帰納法的に無限の階段を上る恐ろしい構図が浮かんでくる。


正しい証明が目の前にある。しかしやたら長い。半端じゃない、なんせ一部屋を埋め尽くす程のプログラムの長さだ。


そんなこと実際起こりえない!とは言えたらよいのだが現代の科学はコンピューターの入らない分野はないのではないかと思えるほどであるし、物理では数値実験と呼ばれる分野もある。私は今回初めて知ったが、数学の分野でも証明にコンピューターを使う一つの分野(?、又は動向)が存在するようである。笑えない。程度の問題はあれこの状況は現実に起こっているのだ。

笑えないのだ・・・・



三平方の定理の証明がいとおしい今宵だ。

P.S.ところで数学者はジョルダン曲線の証明で何を問題にしているんでしょうか?素人にもわかるように問題点を解説してくれる人希望します。いえ難しくてもいいです。多少雰囲気が知りたいだけなので・・

コメント

初めまして

くるるさんはじめまして。
「厄介な証明がマシンリーダブルに書ける」
というのは嬉しいというのはなんとなく分ります。でも数学証明って全てマシーンリーダブルに書けるはずではないんでしょうか? 要は時間の問題じゃないかと言う気がしています。こんな事いっていいのか分りませんが、mizarのようなプロジェクトは今のままでは100年したら潰れているのではないかと思います(汗)。一つの証明をマシーンリーダブルに書き換えるために幾つかのグループが10年かけてやるなんて、まるで「プロジェクトX:関門海峡を作った男達」みたいですね(笑)。 イメージですが、すごい職人軍団があつまって何かをやり遂げたという凄みはありますが、その成果が単なる翻訳だとしたら。。。。。。 プロジェクトXでは関門海峡を作った職人集団は、多くの犠牲者がだし、残った人々もやがて散っていくわけですが、mizarに重なるのは私だけでしょう。

ところで以前からブログチェックさせてもらっています。(内容が高度すぎて理解できないので、チェックしてると言う表現が適切かと)。純粋数学には憧れを感じていますが、いわゆる数学科の数学教育を受けていないもんでなかなか難しいんですが、逆に趣味として気軽に楽しめるという面はあります。

トラックバックどうもありがとうございます。

(1)の意味で証明にコンピュータを使うことはよく聞きますが、(2)はそれで数学を研究するというよりは、まだプルーフチェッカーや自動証明器の研究をやるという形になると思います。

ジョルダン曲線定理の証明は、特別に数学者の間で問題になっているわけじゃないと思うのですが。MIZARによる証明は普通の数学者にとっては、「厄介な証明がmachine-verifiableな形で書けて嬉しいね」以上のことではないだろうと推測します。

コメントの投稿

管理者にだけ表示を許可する

トラックバック

http://letsphysics.blog17.fc2.com/tb.php/192-348755e0

«  | HOME |  »

CATEGORIES

RECENT ENTRIES

RECENT COMMENTS

RECENT TRACKBACKS

APPENDIX

アトム 

アトム 

趣味   近所散策と物理

上記広告は1ヶ月以上更新のないブログに表示されています。新しい記事を書くことで広告を消せます。