▼ 数学を理解する事は難しいと思っている人もいるかも知れないが、 難しいのは省略された暗黙の前提や、説明されていない記号法や演繹則を知らないということに過ぎない。 上記のようなシステムによって全ての細部を記述できるようになれば、数学の証明を理解する事は将棋の棋譜から対局を再現するのと同じ程度に易しいことになるだろう。証明をすることは相変わらず難しいままだろうけど。 （一つの危険性：全く同じ計算結果を出すプログラムが沢山あるのと同じ理由で全く同じ公理系や定理を実装する多数の方法があり得る。この事はここで書いた数学を簡単にするという構想を砕く理由になるかもしれない。ま、等価性は証明できるはずだけど。）
また、上記のようにして全ての前提を明らかにした上で十分ステップの細かい記述にしてしまえば、証明の正しさは、数式を打ち込むその場で機械的に確認することができる。 全てを機械的に検証できるかは知らないが、機械的に検証できないところには"!"マークでも自動で出るようにすれば良いだろう。
この時、数学的な証明は画面の上でマウスでぷちぷちと項を動かしたりするような作業になるだろう。ちょうど将棋ソフトの上で詰め将棋をするような。
数十年後には数学の世界でもこのようなシステムによって書かれた証明で無ければ論文として認められないことになるだろう。
▼ しかし形式的な記号操作に置き換える事が出来ない数学が存在するかも知れないという問題はある。 しかし、私の知識では断言まではできないのだが、多分存在しないのではないかと思う。
たとえば普通図を書いて表現されるユークリッド幾何の問題などは「直線lと直線l'は点Aで交わり」のような言語表現に置き換えられる。従って記号化が可能である。 個人的には複素解析に出てくる contour をどうやって記号化するのか今一つわからないけど、世の中にドローイングソフトが存在するとのを見てるとなんとかなるんじゃ無いかと思ってはいる。
数学の形式化されない部分のもう一つは創造的な部分である。まだ公理の内側にない新しい部分、あるいはまだ証明されていない新しい部分である。これは検証できない変形も許す"!"マークがその存在を許すだろう。これは下で言う「二つの方法」のこちら側（人間側）に stay する理由でもある。
▼ 同じ物に接近する二つの方法
すでに世の中には証明を自動で行うプログラムが昔から研究されている。しかし数学的に難しい定理の証明にはほとんど使われる事が無い。ここで述べたプログラムはそれとは真逆の方法である。
これまでのソフトは「機械が正しいステップを能動的に使って証明する。人間はある程度介入できる」という考えに基づいている。 しかしここで述べたのは「人間が能動的に証明する。機械は正しく無いまたは不明な部分を消極的に指摘する」という考えに基づいている事だ。
これは同じ物にどちらから接近するかと言う問題だ。こういう構造は世界の随所に見られる。
手続き的なモデルを隠蔽して関数的なモデルを構築するか、 関数的なモデルを使って手続き的なモデルを模擬するかとかなんかもこの構造の例だ。 （ここでは状態変更のある計算機モデルを「手続き的」と呼んでいる。）
あるいは、生きているメモリ領域以外はみな死んでいるとするトレーシングガベージコレクションと死んでいるメモリ領域以外はみな生きているとするリファレンスカウントガベージコレクションとかもこの構造の例だ( Bacon, Cheng & Rajan, PDF)。
こういう「同じ物に反対側から接近する二つの方法」があるとき、新しい方に一辺倒の手法が出てきたりする[1]。しかし私の経験からすると大抵は古い方の欠点を修正する方が筋がよいようだ。（GCの例のようにこの議論はあてはまらない例もある。どっちがいい？って言ってもね。）
数学的証明には、人間がするという方法が元からあった上で、機械がするというのが後から現れた。でも機械が全てをするのはあまり上手く行かないようだ。人間が証明する方法の欠点を機械が補うと言う方向の方が筋がよいだろう。
[1] 話が脱線するが社会主義も似たようなものかもしれない。全てが自然の万人の万人への闘争状態の経済があって、それに反対して全てを考えた上でコントロールする経済が構想された。前者にコントロールを加えることも可能であったし、後者に自由を加えることも可能であった。その極限で原理的には二者は同じ程度に良い物になりうる。でも結局筋が良かったのは前者のようだ。
▼ つまり私の立場は数式タイピングソフトから始まって、移項や交換などをGUIで行う機能をつけて、それに等価性の消極的なチェックを入れて行くという立場だ。だから：
1) 人間が読んで理解する事、人間が証明する事が主眼、むしろワープロソフトに似ている
2) 機械は消極的な検証のみ、ルールの逸脱も警告付きで許す
3) GUIとCUI両方で記号変形を行える
以上の話しは現在の時点でもまったく技術的に可能だから、 もしかするとすでにそれに近いソフトは存在するかも知れない。
28日追記：
CoqやAgdaなどの定理証明系について教えてくれた人がいました。（すでに削除されているのは残念だけど。）これら現状についてはサーベイしなきゃね。CoqやAgdaは私の望んでる物とちょっと違ってどっちかと言うと「二つの方法」の向こう側じゃないかと思って調べる事を避けていたんだけど、そうでもないのかな？
先方はシャイな方のようなので直リンクは避けた方がよいと考えましたが、
Coqで４色問題の証明を試みた話を教えていただきました：
Richard Zach,
Four Color Theorem Verified in Coq, LogBlog.
そう言えば、生きているうちにやってる暇があるかは分からないけど、もし自分でそのシステムを作ったらtest runは群論で試してみようと思っている。連続群の分類がちゃんとできるかくらいまで。
数学の限界が計算機の限界を規定する(小飼弾)
これはこの記事への言及記事。こちらについては、私の意見を真逆に誤解した上で、
それに反論して、結局私と同意見になっています。
6月24日（土）
▼ なぜCには標準リスト操作ライブラリが無いのか
と結構長い間ぼんやりと疑問に思っていたんだけど、答えは非常に簡単な事だった。 メモリ管理手法について標準的な方法がないからメモリ管理が必要なデータ構造については標準ライブラリに入れられないのだ。 このようにしてCでは100万のプログラマが100万のリスト操作ライブラリを書く事になった。
C++になってテンプレートが出来て始めてライブラリ化することが可能になったという事か。またC++がテンプレートを持たなければならなかった理由の一つはこれ、つまりメモリ管理を標準化せずにライブラリを書けるようにという事なのだろう。 （あとリストに入れられる物に対する型が厳しいからテンプレート無しではライブラリ化しにくいというのもあるのかも。）
6月23日（金）
▼ やっとこさ論文がでました。よかった。ここまで、つらかった。
Tsuguo Mogami and Keiji Tanaka, Reward Association Affects Neuronal Responses to Visual Stimuli in Macaque TE and Perirhinal Cortices, Journal of Neuroscience, 26:6761-6770
6月22日（木）
▼ 地球低軌道にに複数の望遠鏡を上げて干渉計を構成する計画について技術的に検討している人はすでに存在するのだろうか？
▼ もしかすると素人考えなのかも知れないけど、 文系学術の本質は文献や史料を見つけることと その信頼性について判断する技術なのではないか、 と最近は考えるようになった。
もしそうだとしたら、それを大学の教養の時に学びたかったなと思う。
▼ 最近、この日記を読む人にとっても有益な物にしたいというような風に思うようになった。 私にできる事といえば知識をあげるくらいの事しかできない。しかし知識と言うのはsolidなやつでなければならない。solidでない知識は世の中に混乱を播くだけだし。solidというのは疑いようなくしっかり証明された物を分かりやすく明晰に述べるというような意味だけど。
で、考えてみるに悲しい事に私しか知らないような事なんてほとんどないことに気付く。私がsolidに表現できるような知識なんて、みなすでに教科書がある。そっちを読む方がずっと混乱が少なくてよいかもしれないとか考えたり。
▼ とはいえ、インターネット上に常識的な教科書的な知識があんまり上がってないということもある。「常識的な教科書があればこんな事にはならないのに」というような知識がネットやWikipediaのそこここに上がっていてがっかりするが、そう言うところなら私が寄与しうる事もあるかも知れない。
しかしそうだとしても既存の教科書の劣化コピーみたいな物を書くのは徒労感があるだろうしなあ。「面倒な著作権なんか無ければいいのに」とか乱暴なことを考えたりもする。
6月20日（火）
▼ なぜ最初から作り直したくなるのか
長い間に、プログラムをどんどん機能拡張して行くとだんだんコードが汚くなってくる。ローカルな問題はいいんだけど、とくにデータ構造や大局的なアルゴリズム、プログラム内のインターフェイスなんかが汚くなって、「もう作り直すしか無い」と考えるようになる。
しかし、最初から作り直すのは大抵は間違いだ。地道なリファクタリングで大抵はなんとかなる。 自分でcipherで実践してみてもまったくそう思う。できるはずが無いと思えるようなアルゴリズムの大変革でも連続的な等価変形を積み重ねてできる。そのあいだプログラムは常に動く状態を保てる。
その経験から反対に、なぜ連続的な変形/改良では解決できないように思えるかの原因も分かる。 最終的にどうしたいのかが分かっていれば、大抵は連続的な変形/改良の経路を発見する事ができる。
つまり改良が不可能なような気がするのは、最終的にどうするべきか分かっていないからなのだ。
こういうふうに目標が分かって無いときにこそ、何もかも放棄して作り直したくなるものなのだ。 しかし、目標が分かって無いのに最初から作り直して、それでより良い物を作れるかは疑問だ。
6月19日（月）
▼ 樹状突起をさかのぼる高速の信号の実体は何か？
たとえばHebb学習側では、シナプスに信号が到達して、かつその細胞が発火したときにシナプスは強化される。細胞の発火は細胞体のがついている部分から起きるわけだが、シナプスは最大2mmになることもある樹状突起の上にある。 だからHebb学習のような連合的な学習側を実装するためには細胞体から始まって樹状突起をさかのぼる高速な信号が必要である。 その物理的実体はなんだろうか？
可能性としては化学的なシグナルと電気的なシグナルがある。 しかし低分子でさえ2mmもの距離を拡散するには秒単位の時間がかかるはずである。しかし連合学習にはミリ秒くらいには伝搬してくれなくては困る。したがって化学的シグナルはこの目的には適さない。
電気的な可能性にはふた通りある。受動的な電位と活動電位である。受動的な電位の可能性については例えば Churchland and Sejinovski [1]で論じられているが、受動的な電位が主に考えられているのは1992年当時新皮質では樹状突起上を逆行する活動電位が知られていなかったせいかも知れない。
新皮質について細胞体から始まって樹状突起へと活動電位がさかのぼることがあることは、StuartとSakmann (1994)[2]によって明らかにされている。 またこの伝播が皮質layerごとに時間差をつけた連合を行うのに役にたっているらしいことがLarkumら[3]によって知られている。 ただし、これらは学習つまりシナプス可塑性については何も言っていない[4]。しかしNa+だけでなくCa2+活動電位も関わっていることは可塑性との関係を伺わせる。
以上から個人的には活動電位とくにCa2+の流入する活動電位がその実体の有力候補ではないかと考える。
[1] Churchland and Sejinovski, the Computational Brain, (MIT press, 1992), pp263. 文献は特に代表的だから選んだわけでは無く単に他を知らないだけ。
[2] Stuart GJ, Sakmann B. Active propagation of somatic action potentials into neocortical pyramidal cell dendrites. Nature. 1994 Jan 6;367(6458):69-72.
[3] Larkum ME, Zhu JJ, Sakmann B. A new cellular mechanism for coupling inputs arriving at different cortical layers. Nature. 1999 Mar 25;398(6725):338-41.
[4] 連合的な可塑性については海馬での研究が結構行われている。たとえば Principles of Neural Science, 4th ed., chap63, p1260 のような教科書にもその記述が見られる。
6月16日（金）
6月14日（水）
▼ 失敗する技術の見分け方 ---あるいは技術の屍臭---
うまれる前から死んでいる技術がある。少なくともその一部は屍臭からそれと分かる。以下がそのにおいである。
1) 一つの技術であらゆる問題を解決できるような大言壮語をする。
2) 在来の「腐った」ものを完全に一掃して一から作り直そうとする。
3) 開発が大規模である。
さらに (1)の関連次項として：
・完璧すぎる物を作ろうとする。
・仕様と実装が巨大である。
・勇ましいわりに想定される性能向上が２倍にみたない。
(2)の関連次項として：
・そのあまり互換性、interoperabilityを軽蔑する。
・メインストリームだけが目標である。
(3)の関連次項として：
・小規模な系で実証がされていない。
・大規模になって始めて効率が良くなる（はずであると主張する）。
・最初のリリースが出るまで何年もかかる。
・全てのコンポーネントが揃わないと役に立たない。
・作っている途中に仕様が二転三転する。
・リリースが何度も遅れる。
番外として：
・部分だけだと既存技術にまけてる。
・なんでもできるが既存技術を圧倒するようなニッチや特技が無い。
6月13日（火）
▼ 製本の相場って６千円くらいなのね。今度から利用しようかな。
▼ 古い本の臭いはほぼカビと思われる。本の滅菌をする業者ってないのだろうか。エチレン オキサイドかなんかで滅菌すれば良いと思う。
狂いが出ないように乾燥してくれるともっと良い。 ま、たまに天日干しできればそうまでしなくても良いのだろうけど。
6月12日（月）
▼ 新幹線全面禁煙はやり過ぎだと思う。 私自身は今までタバコを吸った事がない。そして呼吸器が弱かったためタバコの煙には苦しい思いをしたこともあった。
しかし、最近は分煙が進んできてそれほど不快な思いをすることもなくなってきた。 新幹線の喫煙車両から流れてくる煙は確かに臭いが、臭いだけで煙くないので我慢できないほどでは無いし、こちらの我慢のつらさと喫煙者にとってタバコを我慢する辛さをはかりにかけたら喫煙車くらいは許してあげて良いと私は思う。４時間は辛いだろう。
自分が子供のころを思い出すと、たまにタバコを嫌って愚痴を言う人がいたり新聞の投書欄に喫煙への苦情がのってもおおむね黙殺されていたし、喫煙者は誰にも遠慮などしなかった。 それがだんだんと嫌煙の言葉が聞き入れるられるようになり、ついで分煙される場所が増えてきた。
そして最近は嫌煙側の主張が、「問答無用」で通用するようになりつつあると思う。
なるほど、最初はおずおずとあげる弱者の声だった物がいつの間にか問答無用になっていく過程というのはこういう物だったのだなと思った。
この種の弱者の問答無用というのは他にも幾つかあるけど、全過程をみることが出来たのは初めてだ。
また最初に自分が嫌煙側であることを述べたが、もし喫煙側だったらこの文章は同じように読まれないだろう。
どっちの側の発言かで読まれ方が変わるところもアレと同じだ。
T. Mogami
e-mail: mogami@yugiri.bnf.brain.riken.go.jp
