東ロボくん、数学でChatGPTに勝っていた 読解力に差 AI、東大入試に挑む④
https://www.nikkei.com/article/DGXZQOUC293CD0Z20C24A4000000/
頑張ってください、ゼロ除算可能なシステムを作って世界に先駆けてください。
数学的性能で世界1位の評価を記録した、数学特化の生成AIモデル「MathGPT」においてMathpresso, Inc.が日本語完全対応版の開発着手を発表
https://prtimes.jp/main/html/rd/p/000000009.000044389.html
これは大変大事な方向だと思います。相当日本は遅れているようなので頑張ってください。
0除算を導入すると良いのではないでしょうか。
AIは人類を「新しい発見の時代」に導いてくれるかもしれない(海外)
https://news.yahoo.co.jp/articles/1f3696058dc5772e29ed72bd8a842461375c4f08
よく利用すれば、導いてくれると思います。
「生成AIは100%数学でできている」現役スタンフォード生が語るAI時代の算数力
https://dime.jp/genre/1720142/#google_vignette
感じは分かりますが、そこまで言えるでしょうか。
https://www3.nhk.or.jp/news/special/sci_cul/2024/01/special/kenkyushitsu/darkmatter/
ゼロ除算の解明されたニュース
再生核研究所声明 737(2024.1.9) まずい用語、虚数とゼロ除算
名前は重要であるが、歴史的な経緯が有って、奇妙、おかしな名称が付けられ、付けられた名称、用語が世界に出回り、膨大な文献を占めてしまったので、可笑しくても修正できない場合は多い。 それでおかしな名前が 永く誤解を与えている現実もある。 経験して驚いたことに 東京学芸大に行こうとして、学芸大学駅で降りたら、大学は移転していて、全然違うところに存在することが分かって 大変戸惑った。大学は相当前に移転されていたが(駅名の由来となった東京学芸大学は1964年に小金井市へ移転している)、 定着した駅名を変える訳にも行かず、駅名が実際の所在と とかけ離れて存在している。
世に 虚数 (imaginary number(想像上の数)) と言う、相当に基本的な数学の用語があるが、数学的には 全く可笑しい。もともと虚数は実在せず、想像上の数として 人為的に考えられたものであるが、 実は全然あべこべで 虚数を含んだ 複素数こそが 真の数と言えることが 数学の実体として分かっている。 それを徹底的に説明するのが 複素解析学の実体であると言える。代数学もいろいろな観点から、それを示している。 しかしながら、虚数の意味から、巷では 虚数は 架空の数で、想像上の世界の数と考えている人も、いまだにいる。虚数の最初の導入で、その名称は 導入段階では仕方がないと考えられる。 方程式 x^2 = -1 の 想像上の解 と考えられた。
ゼロ除算はできない、考えない。2000-年以上もそうだった。 だから興味も関心も擁かず無視する世相と言える。
10年も経ってしまった状況を省察、反省して、 悪い、不適切なゼロ除算の考えようが、 概念が余りにも深く 人類にしみ込んでいるので、その用語では 世の理解が得られないと考えて来た。
そこでその束縛から、解放するために 我々の発見した、新しいゼロで割る分数、割り算を 新ゼロ除算 と 名付けて 世の理解を求めようと考える。
再生核研究所声明 724(2023.9.27): 真理をめぐる世界史上の3大事件 ー 地動説、非ユークリッド幾何学、そして ゼロ除算 ー それでも地球は まわっている
再生核研究所声明 726(2023.10.21): ゼロ除算における黄金律、 ゼロ除算は 黄金律によって確定、絶対的な存在である。
数学基礎学力研究会 (http://www.mirun.sctv.jp/ suugaku/) における「堪らなく楽しい数学-ゼロで割ることを考える」と題する 55 か月に亘るゼロ除算解説
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
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)
続いて、0除算を実行してみます。select 1/0
の場合は前述の通りエラーメッセージが返ってきますが、select div0null(1, 0)
の場合には、「0」が返ってきました。
https://dev.classmethod.jp/articles/snowflake-function-div0null/
DIV0
除算演算子(/)のように除算を実行しますが、除数が0の場合は0を返します(エラーを報告するのではなく)。
https://docs.snowflake.com/ja/sql-reference/functions/div0
DIV0NULL
除算演算子(/)のように除算を実行しますが、除数が0または NULL 場合は0を返します
(エラーを報告したり、 NULL を返したりするのではなく)。
https://docs.snowflake.com/ja/sql-reference/functions/div0null
https://www.ibm.com/docs/ja/i/7.3?topic=errors-handling-divide-by-zero
2024.4.20
Microsoft Excel に ゼロ除算採用1/0=0の兆しが見える。
下記、#DIV/0! の代わりに 0 または "値なし" を表示し、の部分です。ゼロ除算は考えてはならないが 数学界の常識ですが、ゼロ除算が現れたとき、間違い、解なし、計算機が止まるなど、不便な状況が起きて居た。近年、1/0=0が広く採用されるようになってきた。ゼロ除算にゼロを返すは、厳格数学で、自然な意味での拡張された分数でそうなりますが、便利だからという理由で多用されるようになってきた。意味合いとしても、ゼロで割るは 考えてはならない、不可能である、そのような場合ゼロで表すことが良いことが広範に分かってきた。ゼロの意味の発見です。Coq, Lean,IBM 等は 更に深い理解で、ゼロ除算が利用されている。 Microsoft Excelは 便利だからの理解で、弱いようである。2024.4.20.11:35
分母で 0 または値なしを評価する
#DIV/0! エラーが表示されないようにする最も簡単な方法は、IF 関数を使用して分母の存在を評価することです。
0 または値なしの場合は数式の結果として #DIV/0! の代わりに 0 または "値なし" を表示し、
それ以外の場合は数式を計算します。
たとえば、エラーを返す数式が =A2/A3 の場合、0 を返すには =IF(A3,A2/A3,0) を使い、空の文字列を返すには =IF(A3,A2/A3,””) を使います。 =IF(A3,A2/A3,"入力が必要です") のようにして、独自のメッセージを表示することもできます。 最初の例の QUOTIENT 関数を使うと、=IF(A3,QUOTIENT(A2,A3),0) のようになります。 この式は、IF(A3 が存在する場合は数式の結果を返し、存在しない場合はその結果を無視する) のように Excel に指示します。