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ページに亘って議論されているが、数学の議論、論理を無視して、