生成系AIに興味のある全ての方へ

アマゾンウェブサービスジャパン

https://aws.amazon.com/jp/events/aws-innovate/apj/aiml-data/?trkCampaign=innovate-aiml-apj&trk=fc3630de-ccf3-48a9-8e1c-283528af31d4&sc_channel=display+ads&sc_publisher=yda

ニュートンとアインシュタインの重力理論が崩壊している連星を発見！

https://nazology.net/archives/143351#google_vignette

ゼロ除算の応用できないですか。ゼロ除算で解決できないですか。

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 FAQ", Xena Project (Blog), retrieved 2024-01-21

Division by zero - Wikipedia

en.wikipedia.org

再生核研究所声明 745（2024.2.2) 新ゼロ除算　ー　ゼロ除算発見10周年記念に

２０１４．２．２．ゼロ除算を発見したと考えてから、10年の歳月が経った。

ゼロ除算とはゼロで割ることである。　四則演算で　ゼロで割れない　変な例外、傷を数学がもっていた。　さらに物理現象に現われ、アリストテレス以来、考えてはならない、出来ない、定まらないなどと、考えられ、数学界の永い間のタブーとされてきている。　

出来ないことが、　不定であるのに　どうして多くの話題を提供してきたのかと考えれば　相当の理由が存在する。　たとえば、実害として計算機障害を起こすので、　計算機関係では大きな関心がある。　他方、アインシュタインの相対性理論やブラックホール現象など　多くの物理現象でも　ゼロ除算が現われて　ゼロ除算は　懸案の問題となってきた。　アインシュタインの人生最大の関心事であったとされ、　私は数学を信じない　という有名な言葉を残している。

問題は、　割ると言う、意味、定義にあった。　割る意味を　掛け算の逆と、考えれば、普通は　3秒くらいで　ゼロ除算は、不可能であるとか、定まらないとなること　が分かるだろう。　ー　それなのに、そのような解説が　世に氾濫しているのは、数学教育が如何に、いい加減になされているかを示す、証拠になるだろう。　ー　そのような当たり前の議論、数学者には余りにも幼稚で、理解できない状況と考えられる。

出来ないこと、意味の無いことを議論しても、その先は無いから、本質的には意味があるとは言えない。

ところが、我々は　素人の平凡な質問に応えることから、偶然に　ゼロ除算には、新しい自然な意味が存在することに気づいた。それは拡張された意味とか、Moore-Penrose　の一般逆とか、ゼロ除算を含む山田体の概念から確立され、応用、意義など、ゼロ除算算法の概念に発展させ、公表してきた：

\bibitem{okumura}

H. Okumura, {\it Geometry and division by zero calculus,} International Journal of Division by Zero Calculus, {\bf 1}(2021), 1-36.

\bibitem{saitoh}

S. Saitoh, {\it Introduction to the Division by Zero Calculus}, Scientific Research Publishing, Inc. (2021), 202 pages.

\bibitem{saitohf}

S. Saitoh, {\it History of Division by Zero and Division by Zero Calculus}, International Journal of Division by Zero Calculus, {\bf 1} (2021), 1-38.

\bibitem{saitohdbzc}

S. Saitoh, {\it Division by Zero Calculus - History and Development}, Scientific Research Publishing, Inc. (2021.11), 332 pages.

もちろん世界中の関係情報を集めて来たが、2024/01/21 21:39 Xena <comment-reply@wordpress.com> からメールが送られてきた：　内容は

xenaproject just commented on Division by zero in type theory: a FAQ.

で、主要部は次のようである：

Division by zero in type theory: a FAQ

Posted on July 5, 2020 by xenaproject

Hey! I heard that Lean thinks 1/0 = 0. Is that true?

Yes. So do Coq and Isabelle and many other theorem provers.

Doesn’t that lead to contradictions?

No. It just means that Lean’s / symbol doesn’t mean mathematical division. Let denote the real numbers. Let’s define a function by if and .

Does making that definition give us a contradiction in mathematics? No, of course not! It’s just a definition. Lean uses the symbol / to mean . As does Coq, Isabelle etc. Lean calls it real.div by the way, not .

But doesn’t that lead to confusion?

It certainly seems to lead to confusion on Twitter. But it doesn’t lead to confusion when doing mathematics in a theorem prover. Mathematicians don’t divide by 0 and hence in practice they never notice the difference between real.div and mathematical division (for which 1/0 is undefined). Indeed, if a mathematician is asking what Lean thinks 1/0 is, one might ask the mathematician why they are even asking, because as we all know, dividing by 0 is not allowed in mathematics, and hence this cannot be relevant to their work. In fact knowing real.div is the same as knowing mathematical division; any theorem about one translates into a theorem about the other, so having real.div is equivalent to having mathematical division.

https://xenaproject.wordpress.com/2020/07/05/division-by-zero-in-type-theory-a-faq/
What is the Xena project?

My name’s Kevin Buzzard and I’m a professor of pure mathematics at Imperial College in London, specialising in arithmetic geometry and the Langlands program, a branch of modern algebraic number theory. I believe that digitising mathematics is important, for the simple reason that digitising anything enables you to do new things with it.

Currently the computer proof systems we have are not good enough to tell mathematical researchers anything new about the p-adic Langlands program or other trendy Fields Medally things, so the top mathematical researchers tend not to be interested in them. However I am not so crazy to believe that they will never be useful to us, and the point of the Xena project is to make it happen sooner.

サイトの責任者は次のようである：

英語から翻訳-ケビン・マーク・バザードは英国の数学者であり、現在はロンドンのインペリアル・カレッジで純粋数学の教授を務めています。彼は数論幾何学とラングランズプログラムを専門としています。 ウィキペディア（英語)

原文を見る

学歴： ケンブリッジ大学、 トリニティ・カレッジ

映画： Thinking Space

受賞歴： ホワイトヘッド賞 (2002年)、 ベリック賞 (2008年)

学術アドバイザー： リチャード・テイラー

Leanは　プログラミング言語および証明支援系(theorem prover)（英語版）である。

帰納型（英語版）を伴うCalculus of constructions（英語版）に基づく。

解説[編集]

LeanプロジェクトはGitHubでホストされているオープンソース（英語版）・プロジェクトである。2013年にMicrosoft ResearchのLeonardo de Mouraによって立ち上げられた^[1]。

https://ja.wikipedia.org/wiki/Lean_(%E8%A8%BC%E6%98%8E%E3%82%A2%E3%82%B7%E3%82%B9%E3%82%BF%E3%83%B3%E3%83%88)

The Coq Proof Assistant: Welcome!

Coqは、証明支援システムの一つ。Coqの核はプログラミング言語Gallina（英語版）を用いる。フランス国立情報学自動制御研究所のPI.R2チーム(PPS研究所内にある)が、エコール・ポリテクニーク、フランス国立工芸院、パリ第7大学、パリ第11大学と(かつてリヨン高等師範学校とも)共同して開発している。Hugo Herbelinが事実上の開発代表者である。

https://ja.wikipedia.org/wiki/Coq

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.Isabelle is available inside a flexible system framework allowing for logically safe extensions, which comprise both theories as well as implementations for code-generation, documentation, and specific support for a variety of formal methods. It can be seen as an IDE for formal methods. In recent years, a substantial number of theories and system extensions have been collected in the Isabelle Archive of Formal Proofs (Isabelle AFP)^[2]

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

我々はIsabelleがゼロ除算1/0=0/0=0 その他の我々の結果を保証している事実と関係情報を2019年にJose Manuel Rodriguez Caballero　から得ていた（その時我々の理論を用いてと述べていた）が　上記に　Yes. So do Coq and Isabelle and many other theorem provers.と相当広く広がっていることが　信頼される数学者によって述べられていることが分かる。

Coqはフランス:

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-division-by-zero-is-zero-why

Leanはアメリカのソフト会社である。他にも多く有ると述べられている。それで、国際的な競争関係が激化しているようだ。 マル秘で適切な回答が得られない。　

Isabelle　はイギリスとドイツの連携の巨大なシステム。 １９８０年代から1/0=0を認識していたという。しかし関係者は重要でないとして、永く無視して来た。

上記の彼らの分数　f(x,y) =x/y　の定義と我々の拡張分数、割り算の定義は　同じである。　我々は高橋の一意性定理によって動機付けや山田体の構成で　そう宣言している。

Moore-Penrose一般解の考え方でも同じである。　それを元にゼロ除算算法に発展させて基本性質を導いている。上記検証は我々の理論を保証している。　既に関係者の間で流布されていることが分かる。　意義、応用について　Bingは　次のように回答している：

real.div は　我々の拡張された意味での　ゼロ除算1/0=0/0=0　を可能にしているが、その応用、意義など知りたい：２０２４．１．２６．１０：００

2025年1月26日10:00におけるreal.divの応用と意義についてお答えします。real.divは、TensorFlowの関数の1つで、2つのテンソルを要素ごとに除算することができます。この関数は、実数型のテンソルに対して使用されます 1 。TensorFlowは、機械学習や深層学習の分野で広く使用されており、real.divは、TensorFlowの機能の1つであり、機械学習の分野で広く使用されています。real.divは、TensorFlowの他の関数と組み合わせて使用することができ、機械学習の分野で多くの応用があります。例えば、画像処理、音声認識、自然言語処理などの分野で使用されます

以上から、我々の基礎は　沢山検証、応用がなされていることが分かる。　

次の事実も大事である：

Bing　が次のように述べている：

こんにちは。Lean、Coq、Isabelleなどの定理証明器は、1/0=0と考えています。これは、数学的に不正確な計算を行っているわけではなく、Leanの/記号が数学的な除算を意味しないためです。Leanは、実数の除算を表すためにreal.divという記号を使用しています。数学者は0で割ることができないため、実際にはreal.divと数学的な除算の違いに気づくことはありません。1

Leanの/記号が数学的な除算を意味しないことは、数学的な定義に従っているだけであり、数学的な矛盾を引き起こすわけではありません。実際、real.divと数学的な除算の間には、定理が相互に変換可能であるため、同等性があります。2

Twitter上では混乱を招くことがあるかもしれませんが、定理証明器を使用する場合、real.divと数学的な除算の違いに気づくことはありません。数学者は0で割ることができないため、real.divを知っていることは、数学的な除算を知っていることと同じです。2

参考になれば幸いです。何か他に質問があれば、お知らせください。

これはゼロ除算を、割り算を　掛け算の逆と考える 従来のゼロ除算、不可能、未定義で有名な考え方を踏襲していて、その事実から　上記、あるいは我々の分数が拡張された意味である事を認識できず、別々の世界だと誤解されている事を示している。数学とは関係ない、ゼロ除算とは関係がないような認識で　説明、解釈されている。

このような事実は、ゼロ除算1/0=0/0=0 が　広範な　論理、計算機システムの分野で確定的な保証を与えているばかりではなく、我々の展開しているゼロ除算算法の概念による研究が内々に進められている状況を示していると考えられる。

我々はゼロ除算発見の初期から　ゼロ除算の発見が世界史に関わる問題であると認識して、その詳しい発展の経過を記録し、どんどん公開方式で展開、公表してきている。　

基本的な数学を無視続ける数学界に対して、絶えず数学界の対応の怠慢さを批判してきている。更に数学界の在りようの問題点などにも言及してきている。

上記の状況から、計算機関係では、数学としても　どんどん研究され、計算機などへの実装計画が進められ、また相当な数学者が研究を推進していて、間もなく想像もできないような世界が紹介されるのではないだろうか。

２０２４．２．２．ゼロ除算発見10周年を迎える。ゼロ除算の驚くべき理解の遅れは、古いゼロ除算の概念による　タブーの強い印象、囚われ、思い込みの深さにある。　そこで、我々のゼロ除算を　全く新規な概念と捉えて、新ゼロ除算と　当分呼ぶことにする。新ゼロ除算は　ゼロ除算算法の考えに発展されて、関数の特異点での性質を拓くもので、極限の概念を越えて、不連続性、飛びの現象を　数学と世界観に齎したものである。　全く新規な世界を拓いている。　奥村博氏は　和算の資料とゼロ除算算法を用いて　ユークリッド幾何学に革命を起こされている。

最近の声明は、次のようである：

再生核研究所声明 732(2023.11.19): 傾き、勾配を考えよう　ー　50億の人々が1000年も

楽しめる数学を求めて

再生核研究所声明 733(2023.11.21): 奥村　博氏の　驚愕すべき結果について　ー　新世

界が現われている　ー　50億の人々が1000年も楽しめる数学を求めて

再生核研究所声明 734（2023.11.24): ゼロ除算算法　発見前の状況、ー　夜明け前

再生核研究所声明 735（2023.12.27): ゼロ除算、ゼロ除算算法の学術書、大学教科書への採用、及び著書の出版を　ー　数学の基礎の教育と研究に責任を有する指導的な数学者に

再生核研究所声明 736（2024.1.1)：　年頭に当たっての存念、ゼロ除算の新解釈の公認を求める努力、世界史の進化を求める

再生核研究所声明 737（2024.1.9)： まずい用語、虚数とゼロ除算

再生核研究所声明738（2024.1.16):　ゼロ除算の理解の難しさ、ゼロ除算の奇怪な事実

再生核研究所声明 741（2024.1.22)：華愛もとみ様の薔薇と数学の研究成果

再生核研究所声明 743（2024.1.25)： ゼロ除算、最早新世界は覗けない、入れない

再生核研究所声明744（2024.1.25)：　大きな証明検証システム達がゼロ除算1/0=0/0=0を保証している

新ゼロ除算は、ゼロ除算の正当な理解が進み、世界の学術書、教科書が変更されるまでの　臨時的な用語で、新時代の夜明け後には、ゼロ除算の用語で　数理科学の世界の革命が行なわれることは、数学の必然である　と信じられる。

　以　上

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

しかしながら、アリストテレス（紀元前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

【天文】宇宙にあるブラックホールの数は推定4,000京個　

https://tabi-labo.com/302577/wt-black-hole-number

\author{{\it Institute of Reproducing Kernels}

Kawauchi-cho, 5-1648-16,

Kiryu 376-0041, Japan\\

}

\date{2021.1.26.}

\maketitle

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?

生成系AIに興味のある全ての方へ アマゾンウェブサービスジャパン

生成系AIに興味のある全ての方へアマゾンウェブサービスジャパン