定理証明支援システムと呼ばれるソフトウェアがあります。呼び方はいろいろあって，証明支援系とか証明支援言語などとも呼ばれています。西側では簡単に Proof assistant と呼ばれていて，これが一番わかりやすいかもしれません。 中身は命題を記述できる言語を用いて計算機で命題の真偽をチェックし（計算機自体が論理演算をするもんじゃねというつっこみはなしで），定理の証明を支援するというものです。CPUの設計段階での回路のチェックとか産業面でも使われているようです。最近話題になったABC予想の証明についても Proof assistant でチェックしてみたらいいんじゃないかと主張する人がいるようです。
Proof assitant の一つに Isabelle があります。これは英独の大学で開発されました。フリーでダウンロードして使用できます。 isabelle.in.tum.de
さて，ここで，研究者向けのポータルである ReseachGate の話に変わります。 www.researchgate.net 私もここに参加していますが，ここで，０除算に関する質問を上げた人がいました。それに対して，Isabelle のユーザーグループの人が，「HOL/Isabelle で任意の数 $z$ に対して $z/0=0$ を導いていて，Isabelleユーザーではこれが当たり前」と教えてくれました。 Isabelle には多くのパーケージ（ライブラリ）が提供されていて，自分の好きな公理系を用いたパッケージを選ぶことができますが，HOL はそのようなパッケージの1つです。彼はその後に以下の式が成り立つことも示してくれました。 $$ \tan\frac{\pi}{2}=0, $$ $$ \log 0=0 $$ $$ {\rm exp}\frac{1}{x}(x=0)=0 $$ これらは，齋藤氏が得ていた結果と一致します。
ということで，我々が主張している0除算 $1/0=0$ が現代数学の公理系に反するものでないことが第三者による計算機システムを用いた検証で既に明らかになっているというお話でした。
