ぼくがコンピューターで数学をするようになった理由

はじめに

ぼくがTwitterでやたら「Coq！ Coq！」と言ってますが、今回はその話です。

暗算ができない、計算は遅い、ミスを連発する

テストでまったく点が取れないタイプでした。

今考えると当然ですが、数学のルールを全然知らない状態で、意味を読み取ろうとしていました。

たとえるなら、ゲームのハードだけ持っていてゲームのソフトを持ってないような感じです。

みんなで共通のルールを使ってるはずだ

数学がわからなかったので、高校の教科書を写しました。

一言一句見逃さないように写したのですが、等号=の変形ができるような気分になっただけでした。

もちろん今考えると完全ではないです。

ただ等号=の変形だけでは説明できないことをしているところがあるというのには気づけるようになりました。

なので、当時のぼくは「みんなで共通のルールを使ってるはずなんだ。なのにぼくだけ知らない」と思い込んで落ち込んでました。

真理値で爆死する

「等号=の変形以外のなにか」を調べるために論理学の本を読んでみることにしました。

最初に取った本でやらかします。

「なるほど。文章を$\vee,\wedge,\Rightarrow,\Leftrightarrow,\neg$で繋げた形にして真理値（真と偽）を計算すればいいんだね」

「$\forall,\exists$っていうのがあったのか。話してるところの中で真理値がわかればいいんだね」

「あれ、$\forall,\exists$のついた式の真理値ってどうやって計算するんだろう」

「ヤバい、なんか$\forall,\exists$に真理値表、使える気がしない」
　
　
　「そもそも数学の文章って　真　理　値　計　算　し　て　な　く　ね　？」

　
　ちなみにその本は推論規則が書いてませんでした。

補足

普通の数学の文章は、どの推論規則を使ったのかをほぼ書きません。

$\Rightarrow$の導入、$\exists$の導入、場合分け、背理法などにそれらしい表現があるくらいだと思います。

もちろん、推論規則を書かないだけで、使ってないわけではないです。

意識して書いてないだけかもしれないですし、言葉にできないけど使っていることもありえるので確認は必要です。

（真理値の計算はモデル理論の話になりますし、モデルの方でどの論理体系を使ってるかみたいな話にもなるので、真理値の計算を無意識でするのは複雑すぎるのでは？という印象はあります）

数学、複雑すぎる

真理値で心を折られてしばらく経ってから、なんとか一階述語論理が使えるようになりました。

さきほどのゲームのたとえでいうと、ようやくゲームのソフトを手に入れた感じですね。

（ちなみに、それまでは証明が推論規則で繋がった論理式の列ということを理解してなかったので、$\vee,\wedge,\Rightarrow,\Leftrightarrow,\neg,\forall,\exists$でぜんぶ繋ごうとする勘違いをしてました。できなくて当たり前）

で、一階述語論理で大学の数学を手計算でやってみたんですよ。
　
　
　全　部　式　に　で　き　る
　
　
　定理を示すたびに「完全に理解した」状態です。

それと連動して自然言語が邪魔になりました。

当時、すでに数式の（現実的、視覚的な）意味を解釈せずに証明してましたから、意味を理解しやすい自然言語が見えると意味を解釈してしまって計算速度が落ちることに気づいていました。

（論理体系を「作る」ために自然言語を大切にするのはわかりますが、論理体系を「使う」なら話は別です）

そんな感じで調子よくどんどん定理を証明してたんですが、

　
　参考書に書いてる証明より、めちゃくちゃ長くない？

　
　元の証明の100倍くらいの長さになったときは精神がおかしくなりそうでした。

無意識に正しいと思っているところを全部書くとそんなものです。

参考書や論文に書いてある内容は理論のアイディアが大半ですし、無意識や明らかと思って飛ばしているところを全部見えるようにしたら、実際の数学はかなりごちゃごちゃしています。

このごちゃごちゃしたものを自分が処理しきれるかという問題に直面しました。

形式的な証明に限った話ではありませんが、証明が膨大になると文字列の探索が難しくなり、自分の処理能力を超えます。

また、計算ミスをしてる可能性もあるので、一つのミスで膨大な証明が壊滅する恐怖と隣り合わせでした。

数学をコンピューターで

コンピューターで数学ができることは知っていました。

当時は仕様を理解できなくて放置してたんですが、長い証明にぶち当たるたびに「自分の手計算は限界がある」と感じていたので頃合いだったのかもしれません。

そこで、定理証明支援系のCoqを覚えて使ってみたら圧倒的と言わざるを得ませんでした。

手計算でやってたことがそのまま出力されてるし、先入観をもたず、ミスもしない記憶力の怪物と自分で証明をダブルチェックしているような状態です。

自分の中で紙や黒板の数学が終わった瞬間でした。

おわりに

ぼくがコンピューターで数学をするようになった理由はこんな感じです。

補足をすると、ぼくはコンピューターを完全に信用しているわけではありません。

コンピューターにバグがある可能性は考えておかないといけないです。

また、コンピューターでできない部分は自分でやらないといけないので、人力の部分はたくさんあります。

ただ安心感は手計算のみの非じゃないので、手計算だけには戻りたくないですね。