ICMS 2006 最終日

朝食は抜き。

Room C の形式的証明の Session 3 を聞くことにする。

Gonthier -- 4色問題に Coq で証明を付けたという話。双対グラフに話を移さずに、境界の合流地点の側に dart という点を打ち、それを境界の内側で結ぶ f という有向グラフと、合流地点を取り囲む n という有向グラフと、辺を横切るように dart を結んだ e という両向きの辺で話を進める。 4色問題は平面グラフの話ということでこのグラフの Euler 数を仮定に入れる。各種直観的な操作をこの f, n, e の話に還元して述べ直し、35行の定義と形式的証明に落し込むことができた。
Avigad -- 実数の不等式の形式証明。実数「体」として扱えば扱えるが、効率が悪いから和に関する推論と積に関する推論に分ける。分けた後で一緒にしようとすると分配法則がないので難しいなあというようなとりとめのない内容。
Hales -- 今度は Kepler 予想の形式的証明。最近解かれたとされているが、数 GB のログを解析しないことには「証明」が確認できないので、いくつかの部分に分けて形式的証明を与える flypick というプロジェクトを進めている。一部 "tame" という部分は証明が終った。 Linear Program の話が残っているがこれが「ログ」の部分。証明のテクニックとして、反例になりそうな配置を箱に入れてその長さを評価すると負の数になるからそのような配置はない、という証明方法を使うらしい。

休憩のあと、 Room B に移動して、Session 1。

Xin Li -- カナダ人。効率的な多項式の実装というタイトルだったが、AXIOM に新しい多項式型を作るに当たって、SPAD から CommonLisp, C, Assembler とコンパイルが進む途中に介入して効率を上げるという話なので、「やりたきゃやれば」。

プラナリー
Harrison -- 形式的証明は役に立つよ。

昼食は横山さん村尾さん井田さんと昨日と同じ所。隣の席にも ICMS 参加者。

再びビデオ係として Session 1。

Sekiguchi, Yamashita, Takato -- Maple のグラフィックスを綺麗にしよう。
Yanami, Anai -- Maple で QE (quantifier elimination)。Matlab とつないで利用。
Iglesias -- 工業に使う視覚化。

最後に Session 3 に戻って、Coq のデモ。 30人もの数学者が 2<>0 をどう証明するか議論するなんて、めったに見られる光景ではないだろう。実数の話なのでペアノの公理は使わないというしばり。本当はもう少し複雑なことを証明していたのだが、形式的証明というのはマゾヒスティックな趣味だということが良く解った。

解散。