José Manuel Rodríguez Caballero Added an answer In the proof assistant Isabelle/HOL we have x/0 = 0 for each number x. This is advantageous in order to simplify the proofs. You can download this proof assistant here: https://isabelle.in.tum.de/ その後 我々が導いていた いろいろな公式について、できるかとの質問に対して 回答があり、 信じられないほどに ソフトが完成されていることを見て、驚嘆させられた。 Isabelle構築の責任者とは 相当以前から交流がありましたが、1/0=0 は convention で大したことではない と 言っていました。 ( - これはゼロ除算算法の著書素案に氏のメールを引用、責任者にも素案を送っている。) しかし、実は 相当なことを 大きな研究グループで ゼロ 除算を発展させた ゼロ除算算法の実装に成功して、 公表している。 2018年8月頃までには完成していたと 考えられる。 (2値 関数が2つの値をとることや 大事な \log 0 =\tan(\pi/2)= \exp (1/x) (x=0) =0 も できているので、驚嘆です。 2019.2.17.20:05)。 ゼロ除算については、発見 (2014.2.2) 後 5年を経過し、論文や国際会議、日本数学会でも公表しているにも関わらず、公には未だ認知されているとは言えず、数学界でも、世間でも ゼロで割ってはいけないは 未だ定説になっていて、インターネット上では 不適当な議論が 毎日のようになされている。 例えば、 S. K. Sen and R. P. Agarwal, ZERO A Landmark Discovery, the Dreadful Void, and the Ultimate Mind, ELSEVIER, AP(2016) が 出版され、我々の初期の論文(2014出版)がIntroductionで2ページに亘って議論されているが、数学の議論、論理を無視して、 “Thou shalt not divide by zero” remains valid eternally. と結論づけ、Brahmagupta (598 -668 ?) の結果0/0=0さえ否定している。そこで、直接ドイツ オーベルバッハ研究所で 不等式の国際会議で会ったことのあるAgarwal 教授に我々の結果を送ったところ、誤りを認めるようなメールを受け取った。 そこで、計算機のゼロ除算可能、成功の歴史的な事実 に関して、簡潔にその意義と所感を纏めて置きたい。 - 出来るだけゼロ除算発展の経過を記録して置くためである。 先ずは、計算機のゼロ除算成功の意味と意義である。計算機がゼロ除算を可能にしたということは、1/0, x/0, 0/0, \tan (\pi/2), \log 0, \exp (1/x)(x=0) など 現代数学では考えられない値 を 計算機が出力として、出していることを意味する。それらの値は、我々がゼロ除算やゼロ除算算法で導いている値である。ゼロで割ったらどうなるか、それは、数値として求める場合と、関数値で求める場合が有るが、 上記計算機、ソフトは ゼロ除算算法を数式処理で解析的に求められるように作られていると考えられる。兎に角、計算機が1/0=0 等を出力したというのであるから、数学では、数学界では考えられない値を出したのだから、その意義は極めて 大きいと言える。- この真相は ゼロ除算算法の結果を出力させる計算機を、ソフトを作った相当なグループがケンブリッジ大学とミュンヘン工科大学周辺に存在するという事実である。そのことは、それらの出力、現代数学では考えてはならない結果を 間違いではなく、意味のある結果であると 評価しているということである。 意味のない結果をドンドン出す計算機システムを公開することは 意味がないだろう。 失敗作として世に出ないのが常識ではないだろうか。そこで、これは相当なグループによる ゼロ除算算法の認知 として考えられる。