数学界を騒がせている SSReflect。
一般の方々は、まだ知らない人も多いのでは。
SSReflectとは証明言語の１つです。
数学の定理の証明を表現できる、コンピュータ上の言語です。
数学者にとって実用的だと感じられるレベルになったのは、
割りと最近のこと。
ですから、一般の方々には、ほとんど知られていないはず。
さて、千葉大学理学部（千葉大学大学院理学研究科）では
数学・情報数理学科（数学・情報数理学コース）
という「数学」と「情報数理学」の両方を同時に扱うことで、
日本での独自の地位を築いてきました。
だからこそ、
SSReflectのように、数学と情報数理学をまたがる最先端の話題が
大学で議論できるわけです。
千葉大学生の恵まれている点です。
そこで、
最先端の話題をみんなで学ぼう！
新しい話題なので、学生も教員も一緒になって勉強しよう！
という意図で、勉強会を企画しました。
３日間、毎日約３時間ずつ。
気力も体力も使います。
学生と教員への呼びかけに、
理学部内に勉強会開催の告知を掲示。
いろいろな人たちが参加くださいました。
学年と役職は
学部１，２，３，４年生、
大学院Ｍ２，Ｄ２、
准教授、
教授、
という幅広い層。
Ｍ１は、集中講義が重なってしまい、不参加になってしまったという。残念。
肝心の勉強会の内容は、
１日目： SSReflectの基本的な使い方。
２日目： 初日の補足＋演習。
３日目： 数学の論文をSSReflectで書き換えていくという話。
という熱い感じ。
あちきは２日目を担当。
演習問題として出したのは、一般的な命題に関する性質。
１．三段論法を証明せよ。
２．命題の（真偽の）可換性を証明せよ。
３．命題の結合法則を証明せよ。
４．命題Ａ，Ｂ，Ｃについて、「ＡかつＢかつＣ」と「ＣかつＢかつＡ」の同値性を証明せよ。
例えば、１問目は
こんな感じで証明されます。
良く見ると５通りの異なる証明が書かれています。
数学の証明は１つじゃない！！と実感できますな。
夏休みが明けたら、
また何か企画しようかな。
できれば、次回からは、
学生が幹事になって運営するような仕組みを作りたいな。
