形式化数学とは？

• 「形式化数学」？？
  「形式化数学」、聞き慣れない言葉だと思います。 それもそのはずで、本格的に一学問分野として立ち上がってからまだ十数年 しか経っていない、まだまだ新しい発展途上の学問分野です。

• 「形式化」って？
  分野のタイトルに「数学」の文字が入っているのですから、何か数学に関係する分野なのであろうことは想像がつくと思います。 では、その前にある「形式化」とはなんでしょう？
  結論を、それもかなり簡潔に述べますと、形式化数学の「形式化」とは数学の証明をコンピュータ言語化することです。
  知っての通り、数学には様々な「定義」や「定理」があります。 そういったものを全て証明付きでコンピュータ言語化し、その正しさをコンピュータで検証(チェック)させるのが、「形式化数学」なのです。
  

• なぜ数学を「形式化」するのか？(その1)
  結論から先に述べれば、
  数学者でも間違いを起こすことはあるから。
  です。
  
  1995年に「フェルマーの大定理（最終定理）」が完全に証明されたとして全世界で話題になったニュースがありました。 この「フェルマーの大定理」とは一体どんなものかというと、
  「3 以上の自然数 n について、xⁿ + yⁿ = zⁿ となる 0 でない自然数 (x, y, z) の組み合わせは存在しない」
  というもので、一見すると非常に単純な問題に見えますが、きちんと（厳密に）証明しようとすると、実は極めて難しいことが知られていた問題です。
  この問題を造った（発見した？）フェルマーとは17世紀のフランス人数学者(1601〜1665)であり、彼はこの問題について
  「この定理に関して、私は真に驚くべき証明を見つけたが、この余白はそれを書くには狭すぎる。」
  と書き残して亡くなってしまいます。
  彼の死後多くの数学者たちがこの問題に挑み続けることになりますが、実に300年以上にわたって未解決のまま残されるというまさに難問中の難問となってしまいました。
  
  結局、20世紀も終わりになってようやくワイルズというイギリス人数学者によって最終的な解決を見るわけですが、その証明法は、ワイルズ自身もＴＶのインタビューで述べていますが、フェルマーが当初想定していたような証明の方法では絶対に証明出来ないものでした。
  なぜなら17世紀当時の数学では存在しない様々な概念や理論を使わなくてはならなかったためです。
  ということは、フェルマーが間違っていたか間違っていなかったか？という２分法で見るならば、このような２分法が妥当であるかどうかはこの際おいておくとして、「フェルマーは間違っていた」という結論にならざるを得ないということになります。
  
  実はこのようなことは数学の世界ではよくある話で、理論を書いた数学者の死後30年も経ってからその理論の証明部分に誤りが発見された、等ということがあったりします。
  このように、後世に名を残すような偉大な数学者であっても人間である以上誤りは起こりえるのです。
  無論、後から誤りが発見されたからといって、その数学者の業績が全て否定されるものではありません。
  
  

• なぜ数学を「形式化」するのか？(その2)
  もう一つお話をしましょう。
  1990年に森重文(もり しげふみ)京都大学教授が（数学のノーベル賞と言われる）フィールズ賞を受賞されたとき、森教授の理論を理解出来るのは世界に10人いない、と報道されました。
  
  それならば、理解出来る人が世界に10人といない理論の正しさを
  一体何処の誰が保証してくれるのでしょう？
  先に述べたように、"偉い人"が証明したからといって、必ずしもそれが絶対に正しいとは限らないのです。
  (蛇足ですが、例に挙げた森教授の業績は既に複数の人間の手によって検証が済んでおり、その正しさは確認されています。)

• なぜ数学を「形式化」するのか？(結論)
  このように数学の世界では、近年何かと話題の意図的なねつ造は論外として、しばしば誤ったままの証明が発表されてしまうということがままあります。
  ところで、数学は同時に最先端の科学・技術を支える強力な道具でもあります。
  我々が日常的に使用するコンピュータなどは言ってみれば巨大な数学の塊と言っても過言ではありません。
  そのコンピュータシステムを支えている数学に、実は誤りがあった、などと言うことがあったらどうでしょう？
  これは大変なことになる、と想像出来ませんか？
  数学を形式化し、コンピュータという敢えて全く融通の利かないものに数学の証明をチェックさせる意義とはまさにこの部分にあるのです。