再生核研究所

我々はゼロ除算の情報を絶えず、探してきた。　初めてゼロ除算が可能で、我々の結果と同じ結果を導いた　計算機システム　が現れた：

２０２３．４．２３．１９。０２

その古い情報は相当前から持っていていた。

Isabelle/HOL　は

ゼロ除算が出来たと言っている。証明も有ると述べている。

数学界は　その計算機システムに　遅れをとっている。

２０２３．４．２３．１３：２７

Isabelle/HOL is a logic of total functions, so there is no built-in notion of a fraction or any other function application being undefined. That is, a / b is defined for all a and b, and it returns their quotient except when b is zero. But then it still has a value.

In the library, the decision was made to complete the function in such a way that x / 0 = 0. This decision simplifies many proofs, since you have to deal with less side conditions. Unfortunately it also sometimes confuses people who expect something else.