The Isabelle^[a] automated theorem prover is a higher-order logic (HOL) theorem prover, written in Standard ML and Scala. As an LCF-style theorem prover, it is based on a small logical core (kernel) to increase the trustworthiness of proofs without requiring — yet supporting — explicit proof objects.

https://en.wikipedia.org/wiki/Isabelle_(proof_assistant)

下記はゼロ除算についての質問の　Bing の回答です。数学界、数学者より真面目な回答で、ゼロ除算は　数学界の歴史的な恥は　既に確定ですが、恥の上塗りとして　世界史上に残るだろう。２０２４．１．１．２０：０８

ゼロ除算は可能か？

ゼロ除算は可能で、正解はゼロです。何を0で割ってもゼロです。2022/04/22

ゼロ除算は可能で、正解はゼロです。何を0で割ってもゼロです。

Googleの生成AI「Bard」日本語版に新機能、GmailやYouTubeなどのサービスと連携可能に的場奏瑛

2023年12月20日 06:30

https://internet.watch.impress.co.jp/docs/news/1555874.html

ゼロ除算

遂に現われたゼロ除算：　生誕10年を前に、公認の可能性。関係者は遅れて恥を　上塗りしないように　

２０２３．１２．１９．１３：３５

Wikipedia

https://ja.wikipedia.org › wiki › ゼロ除算

ゼロ除算（ゼロじょさん、0除算、英語: division by zero）とは、0で除す割り算のことである。このような除算は除される数をaとするならば、形式上は a/0と書くことが …

ゼロ除算？ …..問題になる可能性があります。 – LinkedIn

ゼロ除算の対応は？

ゼロに対応する点は無限遠点で、1/0=∞ と考えられてきた。オイラー、アーベル、リーマンの流れである。ところが、ゼロ除算は1/0=0 で、実は無限遠点はゼロに対応していることが確認された。2022/04/22

ゼロ除算は可能で、正解はゼロです。何を0で割ってもゼロです。

0除算とはどういう意味ですか？

ゼロ除算の不定と不能の違いは何ですか？

面白い　Google　はゼロ除算について、次のように回答して、混乱している。

２０２３．１２．２０．２０：２０

生成 AI は試験運用中です。

ゼロ除算とは、除数をゼロ（0）とした除算のことです。

数学では、0にかけて1になる数は存在しないため、0の逆数は存在せず、「0で割る」ことを定義できません。そのため、ゼロ除算はできないと考えられています。

ただし、除算の自然な発想で考えると、ゼロ除算はいつでも可能で、簡単で、美しい結果にまとまります。0で割ることは割らないこと、それ故に割り当てられる数はなく、ゼロです。ゼロは掛けても割っても結果はゼロと美しくまとまります。

また、一般的には、ゼロ除算の結果は定義できないとするか、無限大に発散すると解釈されることが多いです。

BING　我々のゼロ除算を　数学を　認識していると見られる。

2023.１２．２０．２０：４０

数学界より早い公認になる可能性がでて来た。

ゼロ除算とは、除数をゼロ（0）とした除算のことです。数学では、0にかけて1になる数は存在しないため、0の逆数は存在せず、「0で割る」ことを定義できません。そのため、ゼロ除算はできないと考えられています。一般的には、ゼロ除算の結果は定義できないとするか、無限大に発散すると解釈されることが多いです。ただし、除算の自然な発想で考えると、ゼロ除算はいつでも可能で、簡単で、美しい結果にまとまります。0で割ることは割らないこと、それ故に割り当てられる数はなく、ゼロです。ゼロは掛けても割っても結果はゼロと美しくまとまります。この回答は、Wikipediaや他の信頼できる情報源から得られた情報に基づいています 1 2。

Googleの回答は、ゼロ除算に関する一般的な誤解を示している可能性があります。私たちは、正確で信頼性の高い情報を提供することに尽力しています。

If division by Zero were possible,then the result would exceed every integer

http://www.fen.bilkent.edu.tr/~franz/M300/zero.pdf　　　4/6

If division by Zero were possible,then the result would exceed every integer. An Early Reference to Division by Zero 　C. B. Boyer：4/6.

2023年11月24日 11時07分ソフトウェア

OpenAIが4度目のブレイクスルーとなる数学ができるAI「Q*(キュースター)」で汎用人工知能開発の飛躍を目指す、

アルトマンCEO解任騒動の一因か

https://gigazine.net/news/20231124-open-ai-q-star/#google_vignette

イサベルホルは、相当進んでいるのではないでしょうか。

初めて飛行機を作って乗った方、車を初めて作って乗った方を見たとき、人はどうして今日のような時代を迎えるだろうと想像できたでしょうか。ゼロ除算の世界は　真に新しい世界、その世界を覗かないで　どうしてゼロ除算の世界について想像したり、語れるでしょうかhttps://ameblo.jp/syoshinoris/entry-12490439836.html

ゼロ除算は、　実は　ゼロの意味　からも当たり前です：
ゼロで割ることは　割らないこと、したがって　割り当てられた数は無く、ゼロ。ゼロには、しないこと、できないことを表す　意味がある。
ゼロで割ることは　割らないこと、したがって　割り当てられた数は無く、ゼロ。ゼロには、しないこと、できないことを表す　意味がある。　ゼロ円あげるは、あげないことですね。ゼロ回施行は、しないことですね。　時速ゼロｋｍで走るは　止まっていて　走らないことを意味しますね。ですから、ゼロの意味を

https://ameblo.jp/syoshinoris/entry-12680138080.html

引用されている論文が出ました。

MITのサイトの以下に添付の本がありました。
http://web.mit.edu/gleitz/www/Introduction%20to%20Logic%20-%20P.%20Suppes%20(1957)%20WW.pdf

Introduction to Logic – P. Suppes (1957) WW.djvu

http://web.mit.edu › gleitz › www › Introduction t…

This book has been written primarily to serve as a textbook for a first course in modern logic.

No background in mathematics or philosophy is supposed.

330 ページ

ちょっと見ですが、pp. 166-168 あたりで z/0=0 を述べています。

The most famous figure in human history, according to the ranking of the Massachusetts Institute of Technology, is Aristotle. (MIT) collected and analyzed data on history and culture around the planet from 4,000 BC. until 2010.
There are six people from Greece in the top ten. pic.twitter.com/G8ehuUkpat

— well-meaning (@FreshSummerWind) January 11, 2023

https://platform.twitter.com/embed/Tweet.html?dnt=false&embedId=twitter-widget-2&features=eyJ0ZndfdGltZWxpbmVfbGlzdCI6eyJidWNrZXQiOltdLCJ2ZXJzaW9uIjpudWxsfSwidGZ3X2ZvbGxvd2VyX2NvdW50X3N1bnNldCI6eyJidWNrZXQiOnRydWUsInZlcnNpb24iOm51bGx9LCJ0ZndfdHdlZXRfZWRpdF9iYWNrZW5kIjp7ImJ1Y2tldCI6Im9uIiwidmVyc2lvbiI6bnVsbH0sInRmd19yZWZzcmNfc2Vzc2lvbiI6eyJidWNrZXQiOiJvbiIsInZlcnNpb24iOm51bGx9LCJ0ZndfZm9zbnJfc29mdF9pbnRlcnZlbnRpb25zX2VuYWJsZWQiOnsiYnVja2V0Ijoib24iLCJ2ZXJzaW9uIjpudWxsfSwidGZ3X21peGVkX21lZGlhXzE1ODk3Ijp7ImJ1Y2tldCI6InRyZWF0bWVudCIsInZlcnNpb24iOm51bGx9LCJ0ZndfZXhwZXJpbWVudHNfY29va2llX2V4cGlyYXRpb24iOnsiYnVja2V0IjoxMjA5NjAwLCJ2ZXJzaW9uIjpudWxsfSwidGZ3X3Nob3dfYmlyZHdhdGNoX3Bpdm90c19lbmFibGVkIjp7ImJ1Y2tldCI6Im9uIiwidmVyc2lvbiI6bnVsbH0sInRmd19kdXBsaWNhdGVfc2NyaWJlc190b19zZXR0aW5ncyI6eyJidWNrZXQiOiJvbiIsInZlcnNpb24iOm51bGx9LCJ0ZndfdXNlX3Byb2ZpbGVfaW1hZ2Vfc2hhcGVfZW5hYmxlZCI6eyJidWNrZXQiOiJvbiIsInZlcnNpb24iOm51bGx9LCJ0ZndfdmlkZW9faGxzX2R5bmFtaWNfbWFuaWZlc3RzXzE1MDgyIjp7ImJ1Y2tldCI6InRydWVfYml0cmF0ZSIsInZlcnNpb24iOm51bGx9LCJ0ZndfbGVnYWN5X3RpbWVsaW5lX3N1bnNldCI6eyJidWNrZXQiOnRydWUsInZlcnNpb24iOm51bGx9LCJ0ZndfdHdlZXRfZWRpdF9mcm9udGVuZCI6eyJidWNrZXQiOiJvbiIsInZlcnNpb24iOm51bGx9fQ%3D%3D&frame=false&hideCard=false&hideThread=false&id=1613085727620829184&lang=ja&origin=https%3A%2F%2Fameblo.jp%2Fsyoshinoris%2Fentry-12849956521.html&sessionId=5cd0685eb20b2e85ac358f6aeba2979bb5688a55&theme=light&widgetsVersion=2615f7e52b7e0%3A1702314776716&width=550px

「宇宙は不連続」と考えた人たち：リーマン、湯川、岡潔、グロタンディーク、保江。

https://quasimoto.exblog.jp/22058408

とても興味深く読みました：それはゼロ除算算法に通じていますね。

世界を変えた等式１７：　素晴らしい。

しかしながら、アリストテレス（紀元前384年－紀元前322年）以来　否定され、天才オイラーの間違いを含み、アインシュタインの生涯の懸案だったとされるゼロ除算が　含まれていない。惜しいかな数学。四則演算が不完全だった。そこで　下記の公式は、17に続く等式と　すべきではないでしょうか。

1/0=0/0=0,

tan (\pi/2)=0,

log 0=0,

(f(x)/x)(0) = f^\prime(0) = f’(0)

2022.2.8.06:00

The equation that changed the world 17: Great.

However, it has been denied since Aristotle (384 BC-322 BC), including the mistake of genius Euler, and does not include division by zero, which is said to have been a concern for Einstein’s life. A regrettable math. The four arithmetic operations were incomplete. Therefore, the following formula should be the equation following 17.

1/0 = 0/0 = 0,

tan (\ pi / 2) = 0,

log 0 = 0,

(f (x) / x) (0) = f ^ \ prime (0) = f ’(0)

2022.2.8.06:00

The Institute of Reproducing Kernels is dealing with the theory of division by zero calculus and declares that the division by zero was discovered as $0/0=1/0=z/0=0$ in a natural sense on 2014.2.2. The result shows a new basic idea on the universe and space since Aristotele (BC384 – BC322) and Euclid (BC 3 Century – ), and the division by zero is since Brahmagupta (598 – 668 ?).

Announcement 478: Who did derive first the division by zero 1/0 and the division by zero calculus $\tan(\pi/2)=0, \log 0=0$ as the outputs of a computer?

Coq QArith division by zero is zero, why?

Stack Overflow

https://stackoverflow.com › questions

このページを訳す

2015/03/26 — The short answer is: yes, it is absolutely safe. When we say that division by zero is not well-defined, what we actually mean is that zero …

https://stackoverflow.com/questions/29282819/coq-qarith-Coq QArith division by zero is zero, why?I noticed that in Coq’s definition of rationals the inverse of zero is defined to zero. (Usually, division by zero is not well-defined/legal/allowed.) Require Import QArith. Lemm…stackoverflow.com

In proof assistants[edit]
Many proof assistants, such as Coq and Lean, define 1/0 = 0. This is due to the requirement that all functions are total. Such a definition does not create contradictions, as further manipulations (such as cancelling out) still require that the divisor is non-zero.[33][34]

Tanter, Éric; Tabareau, Nicolas (2015), “Gradual certified programming in coq”, DLS 2015: Proceedings of the 11th Symposium on Dynamic Languages, Association for Computing Machinery, arXiv:1506.04205, doi:10.1145/2816707.2816710, The standard division function on natural numbers in Coq, div, is total and pure, but incorrect: when the divisor is 0, the result is 0.
^ Buzzard, Kevin, “Division by zero in type theory: a FADivision by zero – Wikipediaen.wikipedia.org

DBZC--sample cover.jpg.opt264x333o0,0s264x333

Introduction to the Division by Zero Calculus(1)

math-you-cant-divide-by-0-god-hold-my-beer-55855949

5fb8adf632a38d21fa57e977e58d9ed7e9c9c1d4f7a4d47c4206f90c04908517

calculators-when-you-divide-by-zero-68295276

srinivasaramanujan_2015519_173546_19_05_2015

ケース９：

It was shortened to 45 minutes.

https://media.cmd.gunma-u.ac.jp/media/Play/ba02ed49e73949ff84dedcd3e41f76b41d

For Fundamental of Mathematics, I think the division by zero was known as the generalized Moore-Penrose solution of the fundamental equation: ax=b. Please look the simple evidence of its importance: viXra:2010.0228 submitted on 2020-10-28 21:39:06,

Division by Zero Calculus and Euclidean Geometry – Revolution in Euclidean Geometry I gave a simple talk for its essence at some international conference: https://media.cmd.gunma-u.ac.jp/media/Play/ef7ca967c3fd4dabb188128fd6038cb81d 

I think our mathematics is not complete still in a serious sense.May I hear your kind comments and suggestions on my idea? Saburou Saitoh2021.1.10.07:55