欧米に追いつくために環境整備を中国のAI技術発展には企業や学者の力が不可欠だ先行する

https://toyokeizai.net/articles/-/740797

日本は、、、

27世紀で1000冊の本

哲学、詩から小説、料理本まで、紀元前 6 世紀から紀元後 21 世紀までの 1,000 冊の本

https://www.listchallenges.com/1000-books-in-27-centuries

AIは人類を「新しい発見の時代」に導いてくれるかもしれない（海外）

https://news.yahoo.co.jp/articles/1f3696058dc5772e29ed72bd8a842461375c4f08

よく利用すれば、導いてくれると思います。

「生成AIは100％数学でできている」現役スタンフォード生が語るAI時代の算数力

https://dime.jp/genre/1720142/#google_vignette

感じは分かりますが、そこまで言えるでしょうか。

ニュートン別冊　最新科学でわかる脳のすべて（2024年2月13日発売）

https://www.newtonpress.co.jp/separate/back_biology/mook_240213_2.html

再生核研究所声明 746（2024.2.5) ゼロ除算についての、印象、現況

心を整理するために、ゼロ除算を気分的に柔らかく、おおざっぱに、存念を含めて表現したい。

ゼロ除算を　素人から　簡単な意味を問われて、　思いを新たにしたら、結局、　Moore-Penroseの一般化の解の意味で、　1/0=0/0=0を発見したのが　10年前（２０１４．２．２）である。　気付いたら永くやっていた、チコノフ正則化法の考えで、実は全ては当たり前だった。しかし衝撃は大きく大騒動のような様子であった。　高橋の一意性定理、山田体の考えから、ゼロ除算は我々にとっては当たり前だったが　言えない程の批判が世界中から出たと言える。 しかし、ゼロ除算は当たり前。　しかし　関数y=f(x)=1/x　の原点での値をゼロとする、関数値にゼロ除算を対応させた　ゼロ除算算法が2か月くらいの間に発見され、それが　騒動の第2段階　である。即ち、1/0=0の意味とf(0)=0の意味が本質である。

歴史的に　論理上、 1/0=0 とする可能性が有るとする分析結果があったのは注目すべきである。世界最高と思われる　数学の定理の検証システムIsabelleは　1980年代から1/0=0を認知していたが　関係者はそれは大して意味がないとしてきたと言う。　そのメール、言明を責任者から頂いている。

2019年　我々のゼロ除算算法が正しいとの報告をJose氏から頂き、　論争中の多くのゼロ除算関係者は　その結果を受けて沈黙した。　Isabelleで　我々の理論を用いて、我々の結果を確認したというのだが、その後何か、圧力があったかのように　彼からIsabelleの情報は一切入らなくなってしまった。 そのソフトの部分にsaitohの名前が入っていたが、不明になってしまった。　出力結果はその経過を含めて　広く公開している。　それで、　ずーと1/0=0/0=0　の情報は我々にはどこからも寄せられなかった。　20人くらいの議論してきた仲間がおり、しかも相当な国際会議、論文、雑誌などでも公表して来たのにである。　世に1/0=0/0=0の結果は　我々以外にはなかった。

ところが、突然、

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)

生成系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]

Division by zero - Wikipedia

en.wikipedia.org

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

それを調べたら、我々の意味におけるゼロ除算は real.divの意味で　既に広く用いられていて、広く応用されているというのである。アメリカ、イギリス、フランス、ドイツの大きなシステムが作動しているという。　我々の結果を知らないはずはなく、秘密に関係研究が総合的になされていると感じられる。　彼らがreal.div　が　我々のいう拡張された意味での割り算である認識があるのか否かは　不明だが、独立にやっていると表明すると思われる。　ー　Isabelle　が40年も前に、　認識したことを　数学的に我々は解釈を与えたが、彼らは、我々の理論を知らず、convention として用いたら大いに便利で　力を発揮して　既に応用上確定していると　判断している可能性もある。　言えることは、第2弾　　ゼロ除算算法の概念は、彼らの世界には　現われている様子が見えない。　ー　しかし、10年を経過して沢山公表しているので、すべてを理解したうえで、　どんどん研究を秘密で展開していると考えられる。　何時それらの成果が現われて来るか、分からない状況になっていると感じられる。

上記の世界は巨大だから、1/0=0/0=0の結果は　直ぐにも世界の常識になるのは、既に歴然であると考える。

それは2300年を越える、世界史上の事件であるが、実は衝撃的な事件が　2弾として存在する。何時その扉が拓かれるだろうか。　我々は完全な理論を既に公開している。　充分な証拠を公表している。

どうして、認知されるか、公認されるかの問題に掛かっている。どのようにして公認させようか。　それが当面の問題である。　力なく、我々に残された時間が　そうは無いのが　大きな問題である。　それにしても　我々の知らない内にこうなっていた：

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の他の関数と組み合わせて使用することができ、機械学習の分野で多くの応用があります。例えば、画像処理、音声認識、自然言語処理などの分野で使用されます

我々が述べる　新ゼロ除算　1/0=0/0=0 の応用について　下記のような回答があった：

２０２４．２．４．７：２２

What are the applications of real.div in Lean?

London Clark

Knowledge Empress3h

1. Mathematical Calculations: The real.div function in Lean is used for performing division operations on real numbers. It can be used for various mathematical calculations such as finding the quotient of two real numbers, calculating the reciprocal of a real number, and solving equations involving division.

2. Geometry: The real.div function can be used in geometry to find the ratio of two quantities, such as the ratio of the circumference to the diameter of a circle (π).

3. Physics: In physics, the real.div function can be used to calculate physical quantities such as velocity, acceleration, and force, which involve division operations.

4. Financial Calculations: The real.div function can be used in financial calculations, such as calculating interest rates, compound interest, and mortgage payments.

5. Statistical Analysis: In statistics, the real.div function can be used to calculate various measures, such as the mean, median, and standard deviation, which involve division operations.

6. Machine Learning: In machine learning, the real.div function can be used to normalize data, which involves dividing the data by its mean or standard deviation.

7. Game Development: The real.div function can be used in game development to calculate the movement of objects, such as projectiles, based on their velocity and acceleration.

8. Cryptography: In cryptography, the real.div function can be used to perform operations on large prime numbers, which are often used in encryption algorithms.

9. Control Systems: The real.div function can be used in control systems to calculate transfer functions, which are used to model the behavior of physical systems.

10. Signal Processing: In signal processing, the real.div function can be used to calculate the frequency response of a system, which is used to analyze and manipulate signals.
Have you ever wondered about the various applications of real.div in Lean? Explore the possibilities and dive deeper into this topic by clicking on the link in our bio.

Coqの責任者に著書原稿を送ったところ　返事を頂いた：

2024/01/25 20:35

That's an interesting text. Thanks. Sincerely yours, Hugo Herbelin

　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　以　上

ゼロ除算（ゼロじょさん、0除算、英語: division by zero）とは、0で除す割り算のことである。

このような除算は除される数をaとするならば、形式上は a/0と書くことが ...

関連する質問

0は除算できないのはなぜ？

0による除算とは何ですか？

ゼロ除算は可能か？

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

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

ゼロ除算の対応は？

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

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

ゼロ除算は可能か？

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

linkedin.com

https://jp.linkedin.com › pulse › ゼロ除算は可能で正解...

検索: ゼロ除算は可能か？

0の新しい意味の発見、0の意味から当たり前

0は　できないこと、しないこと、を現す意味をもつ。

0で割る事は割らないことで、したがって

割り当てられた数はない。

すなわち、0除算は０です。

何を0で割っても０です。

100割る0は？

この意味で割り算の意味を考えれば、１００割る０は０であるとなる。2022/04/19

記号∞ （アーベルなどはこれを 1 / 0 のように表記していた）で表す。

https://www.google.co.jp/search?sca_esv=593347961&hl=ja&q=%E3%82%BC%E3%83%AD%E3%82%92%E5%89%B2%E3%82%8B&sa=X&ved=2ahUKEwi1pb26j6eDAxWdhq8BHQSEAMUQ1QJ6BAg2EAE&biw=1600&bih=773&dpr=1

a がゼロでなければ、分数b/aは現代数学の定義と同じに定義される。１００割るゼロはゼロ、すなわち、100/0=0である。2021/11/28

1970年代の教科書でも、ゼロ除算の扱いは同様である ...

ゼロ除算とは何か

それはゼロで割ることである。ゼロで割る事とは何か。　

その定義、意味が　問題である。

それを普通の掛け算の逆と考えれば、それはできないとか、定まらないと　なり、それが永い間の世の常識である。

ところがゼロで割るという意味には、割ることの意味を　自然に拡張（ある一般的な意味における割る意味で）、あるいは　そもそもゼロの意味から、考えると、ゼロ除算は何時でも可能で、何時でも　ゼロで割ればゼロである　という美しい数学が　２０１４．２．２．に発見された。　それを発展させた　ゼロ除算算法　は　数学の基礎に甚大な影響を与え、数学ばかりではなく、人生観、世界観に　甚大な影響を与えることは分かってきた。

特に、数学は　そもそも基本的な欠陥を有している　と言える。

２０２４．１．１０．５：４６

極限ではなくて、ずばりである。　特異点そこで　である。　

近づきでは　幾ら近づいても　特異点での性質は　捉えられない。

２０２４．１．１５．８：５０

インド出身の偉大な　世界的な　指導的な数学者が、ゼロ除算の我々の発見の凄さ　を認識したようである。

２０２４．１．１５．８：４２

I am surprised to have your mail again. I am happy and fully convinced with the great work of scholars Brahmagupta, Bhaskara II, Mahavira, Aristotle, Cauchy, Weierstrass, Euler, Newton, Bernoulli, and their numerous followers. They laid the correct foundation of Mathematics by showing that 0/0 is indeterminant, i.e., it is defined only in the limiting sense.

You will be able to contribute to mathematics on world history with India's great and long hirosophy.

We Japanese studied deeply from India.

I expect your contribution to the division by zero.

My feelings are almost void.

NOT LIMITTING!!!!

I attached one typical evidence.

2024.1.15.8:30

東大合格率とゼロ除算：

ある名門高校の東大合格率は40％だという。　これは架空の話しであるが　東大受験した高校生の合格率と考えれば ありそうな話しであろう。　合格しなそうな人は 受験しないからである。名門校となれば データや経験から、合格率を高められるだろう。

問題は、受験生がゼロの時、合格率はどのようになるだろうか。

現代数学では、考えてはならないとなっている。ゼロで割れないからである。

歴史上はじめて 宣言された我々のゼロ除算では、合格率は ゼロとなる。

世相でも　良い結果ではないだろうか。ゼロ除算不可能を　可能にしている。

ついでに　私の理解に寄れば、　母校の中学は　再編後前も　歴史上　東大受験生は唯一人で　合格している。

東大合格率は１００％である。　甥の同級生で子供のころから　神童の誉が高かった。

母校の高校　再編後前も　歴史上　東大受験生は　ゼロで、従って東大合格率は　ゼロである。　

買い物から帰って　この構想が湧いた。

２０２４．１．１８．１２：３４

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

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

時速ゼロｋｍで走るは　止まっていて　走らないことを意味しますね。ですから、ゼロの意味を

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

何故ゼロ除算が不可能であったか理由

１　割り算を掛け算の逆と考えた事

２　極限で考えようとした事

３　教科書やあらゆる文献が、不可能であると書いてあるので、みんなそう思った。

Matrices and Division by Zero z/0 = 0

http://file.scirp.org/pdf/ALAMT_2016061413593686.pdf

「マイクロソフト」「Google」「Amazon」AI三つ巴戦の行方は？　超絶進化で仕事は奪われサイバー犯罪も激増？https://news.yahoo.co.jp/articles/78d81b626b1ead633347f036e78d32db918f91eb

キラー問題もスラスラ…「韓国製数学ＡＩ」、ＣｈａｔＧＰＴ抜き世界評価１位

https://news.yahoo.co.jp/articles/7bf80224fc9de6702d7540c6a78d3bd693619106

ゼロ除算の５W５H：