形式化数学記述言語Mizarを用いた演習
演習テキスト
なぜmizar？とのご質問にお答えして：
なぜmizarを重視しているのか，特に教育指導に取り入れているかとのご質問がありました。うまく説明できるか判りませんが，以下にある方の学位論文の一節や 小生らの国際学会で講演原稿の一部を引用などしてお答えしておきます。 念のため申し添えますが，以下は小生の個人的見解です。
【学位論文の一節】
今後も発表され,また増え続ける数学・応用数学の諸定理の証明の正しさを人手によらず,計算機で,
検証する手段を持つことは,数学に限らず,数学を基礎とする,工学,科学にとって重要な課題である。
1931年に発表されたエルブランの著名な論文『算術の無矛盾性について』が1960年代に証明の誤りが
発見されその修復がなされた逸話は有名である。 無論，エルブランの偉大な功績が
その誤りによって損なわれることはない。 しかしながら，世界中で発表される科学論文の正しさが，
人手によってしか検証されないとしたら，その膨大さゆえに今後深刻な課題を抱える事になる。
権威あるとされる論文誌に掲載され，あるいは，著明な学者による論文ということで『権威』
を信頼する危険性は無視できない。
Science やNature などの論文誌に，その分野の著明学者が共著者として発表し，世界中から
注目された複数の超伝導関係の有名論文が全くのデータ捏造であったことが発覚した最近の事例をもってしても
明らかである。
まして，そのような実験物理系の研究とは異なり，それらの工学,科学を基礎として支える
数学の研究成果が誤りを含んでいたら，極めて深刻な事態になろう。
意図的な捏造は論外としても，推論誤りなどは常にありうるし，現状のように，極めて細分化された研究分野で
は少し分野が異なるだけでその内容が理解できないということもあり，まして誤りの発見など難しく，
結局同一研究テーマをもっている極めて少数の研究者によって検証がなされるということになる。
正さは権威によっては保証され得ない。それ故に冒頭で述べたように諸定理の証明の正しさを人手によらず,計算機で,
検証する手段を持つことは，今後の科学の発展にとって極めて重要な課題である。』
【国際学会の講演原稿(和訳)の一部】
e-learningが話題になり，視覚効果に訴えたWEB教材，コンテンツが，目新しくもない状況になっているが，
それらは，e-learning・インターネット遠隔教育の手段の一つに過ぎない。その根底にある，従来の講義室で
の集合教育から，教育の個別化への流れこそ重視するべきであろう。個別化の究極には，教員と学生の
一対一あるいは(その学問分野を専門とする教員集団と一人の学生といった)多対一教育があるだろう。
インターネットによって時空を制約を離れば，そのような個別教育は現実に可能である。
この場合，教員は，教育者としてより，ネット上の教材を通じて学習を行う個々学生を手助けする，
コーチしての位置づけされるようになるだろう。
e-learningについて，良く言われるのは，知識の伝達手段しては有効であっても，思考の過程，問題を解析する思考法の演習には不向きであり，従って，論理的思考を根拠とする，自然科学，理工学系の教育に適用できないというものである。
無論，具体的な対象の観察や，実験装置を操作しなければ得られない経験もあり，それらは仮想現実に置き換えることはできないであろう。 従来の教育法と同様、e-learningが万能な特効薬でないことは当然である。
しかしながら，論理的思考，数理的思考訓練についてならば筆者らは以下のような道具を用いている。
例えば，大学の１，2年次の課程での，基礎的な数学定理の証明ですら，これを，学生に正確に理解させるには，担当教員の相当な忍耐力を前提にして，学生の個別の進度に応じた，長時間にわたる徹底した指導が必要になっている。理工系ばなれが深刻化し技術立国が根底から地盤沈下し始めている現状を回復する鍵は，筆者には，論理思考重視の教育以外ないように思える。しかし，現状の大学制度で，そのような，個別または，ごく少人数の学生に対する教育を行う教員をどうやって確保するのか。 また，そのように教員の長時間の忍耐を要求する個別教育は果たして可能であろうか。 誤解を恐れずに言えば，受験勉強で恐らくは重大な発達障害を受けてしまった論理思考能力のリハビリは可能であろうか。計算能力を向上させるために多数の問題を繰り返し解かせるといったような単純な解決法はない。仮に基礎的な定理の証明問題をレポートで回答させたとしても，計算問題とは異なり，解は一つとは限らない。学生の証明を正しいものに直させれば，学生の数だけ定理の証明がある。 それを根気良く，個々の学生の答案について，それが正しい証明になるまで，繰り返し正確に添削をし続ける精神努力は，一体何時まで続けられるであろうか。 このように考えたときに，筆者らは，数理的思考訓練の手段として，疲労を知らない計算機を援用しなければならないことに行き着いた。
筆者らは，以前からポーランド人数学者が開発した形式化数学記述言語を用いて現行の数学定理のライブラリ整備を推進するmizarプロジェクトに参画している。mizarシステムは，プルーフチェッカーと呼ばれるもので，第一階述語論理とTarskiの集合論の公理系をもとに，数学定理の証明を記号論理学レベルで記述し,それの，論理的正しさを計算機によって検証する。
例えば，以下はその記述の例である。
environ
vocabulary
ARYTM_3, :: divides
ARYTM_1, :: -
INT_1; :: Integer
notation
XCMPLX_0, :: *
REAL_1, :: -
NAT_1, :: Nat
INT_1; :: Integer
constructors
REAL_1, NAT_1, INT_1;
clusters
INT_1; :: Nat -> Integer
requirements
SUBSET, NUMERALS, :: numerals are Nat
ARITHM; :: basic computations
theorems
INT_1, XCMPLX_1;
schemes
NAT_1;
begin
theorem
for n being Nat holds 2 divides n*(n-1)
proof
defpred P[Nat] means 2 divides $1*($1-1);
0 = 2 * 0;
then
P0: P[0] by INT_1:def 9;
PN: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume P[n];
then consider s being Integer such that
A2: n * (n - 1) = 2 * s by INT_1:def 9;
(n+1)*(n+1-1) = n*(n-1) + n + n*1
.= 2*(s+n) by A2;
hence P[n+1] by INT_1:def 9;
end;
thus for n being Nat holds P[n] from NAT_1:sch 1(P0,PN);
end;
INT_1は既にmizarシステムに登録済みのライブラリであり
INT_1:def 9は 以下のような定義が記述されている
definition
let i1,i2 be Integer;
pred i1 divides i2 means
:: INT_1:def 9
ex i3 st i2 = i1 * i3;
reflexivity;
end;
同様に，NAT_1:sch 1は以下の登録済みの数学的帰納法の公理図式を表している。
scheme Ind { P[Nat] } :
for k being Nat holds P[k]
provided
P[0] and
for k being Nat st P[k] holds P[k + 1];
mizarの文法の詳細は，
同僚の解説書 を参照願いたいが，上のbegin 以下の記述を眺めれば，記号論理の表現に，予備知識がある読者の方なら，
Natが 自然数を表すものと知れれば，
『任意の自然数nについて，２は n*(n-1) を割り切る』
という，命題とそれの数学的帰納法による証明を記述していることが大よそ判読できるであろう。
mizarはこのように，自然言語に近い表現ができることが，特徴である。この種のプルーフチェッカー
自体は世界中に何十種類とあるが，それらは大学院の学生が卒論でつくって，それでその学生が卒業
したら誰も使わなくなってしまったようなものがたくさんある。 その中にあって， Mizar はワルシャ
ワ大学の Andrzej Trybulec 教授を中心とした Mizar グループによって，多くの研究者や大学院生など
がそれに協力してライブラリを増やしている．
現在800程度の，数学ライブラリが整備されており，そのシステムと
ライブラリは
インターネット上で全て公開されている。 このMizar グループの日本側の代表者である中村教授と筆者らは
同時にインターネット大学院の運営に参加している。 その教材には，mizarが重要な位置を占めているが，
mizarシステムはネット上で，学内，学外に限らず公開されている
学生は，このシステムを使用して，プログラム実習のように，上記のような，簡単な命題の証明から，
下記の教養課程１,２年次の微積分などの定理の証明を記述する演習を受ける。
theorem
for n be Nat, f be PartFunc of REAL,REAL, x0,r be Real st
( 0 <r & f is_differentiable_on n+1, ].x0-r,x0+r.[ )
ex s be Real st 0
f.x=Partial_Sums(Taylor(f, ].x0-r,x0+r.[,x0,x)).n
+ (diff(f,].x0-r,x0+r.[).(n+1)).(x0+s*(x-x0))
* (x-x0) |^ (n+1) /((n+1)!);
プログラム言語の演習と異なり，記号論理を知られる読者であれば，少々長い数学定理の証明を記述させれば，
行き当たりばったりに証明を考えても，その安易な計画性のない試みは挫折し，最初から証明を組織的に考え，
途中経過に，適当に補題を配置するなど,論理思考の積み重ねを余儀なくされることは容易に御推察できよう。
証明の記述であるから,『解』は一通りには決まらない。与えられた公理や既に証明済みの定理から
論理的に結論を導ければ良いので, 回答者の数だけ証明もあるといってよい。
例えば，上の簡単な例ですら，n * (n - 1) を 2*(s+n) に変形する過程は幾通りかあるだろう。まして，少々複雑な
証明問題なら，証明の組み立て方自体が種々なものになり，学生の数だけ答案がある。そのような課題を，
レポート添削に形で,教官が添削したら相当な時間が必要であろう。しかも全ての学生が,正しい証明を書いてくるまで,
繰り返し答案に添削を正確に行うことは余程の努力が必要であろう。
このプルーフチェッカーは，計算機の処理能力が許す限り，同時に何人の学生でも利用できる。
また，学生のノートPC上でも動作できる。
疲労をすることなく，感情的になることもなく，機械的正確さをもって学生の証明が完成するまで，何万回でも添削し続ける。
ライブラリは,今後,IT院生らも参加するmizarプロジェクトによって一層の充実が図られていく。
無論，将来は，殆どの数学定理のライブラリ化が完成し，数学，数理科学，応用数学分野の研究者が，
mizarを用いて自分たちの最新の研究成果とその証明を記述できるようになるだろう。
証明の正しさは，どのような無名な研究者の論文であっても，学会の権威者ではなく，計算機が，瞬時に判定する。
従来の人間の査読は人間系によってのみ可能な結果の有用性といったより高度な判定に利用される。
学問研究の数理科学分野でのユビキタスが実現されるであろう。
【古い手法？ 数学は最古の科学ですが。。。】
『IT分野の研究・開発に深く関わる数理的技術は多岐にわたっており，Mizarのような形式的手法はその一翼を担っているに過ぎない。さらに，近年においては，形式的手法，特に自動検証の技術の進展は目覚ましく，汎用の定理証明技術だけでなく，モデル検査，充足可能性判定，静的解析，抽象解釈などの個別の技術の進歩が顕著となっており，Mizar自身の技術は既に古典的なものとなっている。』とのご批判がある方々からあったようですが，
これは『目的』 と『手段』を 全く混同されているようです。 実際，
上記文中の mizar を 形式化数学 あるいは もっと単純に数学 という 言葉に置き換えてみていただければ ご理解頂けると思います。 数学は 古典的どころか２０００年以上まえから 科学に採用されてきた手法なのですから。
問題なのは 『モデル検査，充足可能性判定，静的解析，抽象解釈』
などの手法自体の正しさは，どうやって検証するのかということです。 まさか 著名な その分野の研究者が 提案している手法だから，あるいは著名な雑誌に掲載されたから をその根拠にはできないでしょう。
小生らは 計算機検証による形式化数学という手法を用いて，より信頼しうる『厳密な正しさ』のもとに それらを再構築することの必要性を認め 緊急かつ重要な課題と考え，研究教育活動をしています。
