数学的性能で世界１位の評価を記録した、数学特化の生成AIモデル「MathGPT」においてMath

数学的性能で世界１位の評価を記録した、数学特化の生成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

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

2024年に大注目の科学は？

https://www3.nhk.or.jp/news/special/sci_cul/2024/01/special/kenkyushitsu/darkmatter/

ゼロ除算の解明されたニュース

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

名前は重要であるが、歴史的な経緯が有って、奇妙、おかしな名称が付けられ、付けられた名称、用語が世界に出回り、膨大な文献を占めてしまったので、可笑しくても修正できない場合は多い。　それでおかしな名前が　永く誤解を与えている現実もある。　経験して驚いたことに　東京学芸大に行こうとして、学芸大学駅で降りたら、大学は移転していて、全然違うところに存在することが分かって　大変戸惑った。大学は相当前に移転されていたが（駅名の由来となった東京学芸大学は1964年に小金井市へ移転している）、　定着した駅名を変える訳にも行かず、駅名が実際の所在と　とかけ離れて存在している。

世に虚数　(imaginary number(想像上の数）) と言う、相当に基本的な数学の用語があるが、数学的には　全く可笑しい。もともと虚数は実在せず、想像上の数として　人為的に考えられたものであるが、　実は全然あべこべで　虚数を含んだ　複素数こそが　真の数と言えることが　数学の実体として分かっている。　それを徹底的に説明するのが　複素解析学の実体であると言える。代数学もいろいろな観点から、それを示している。　しかしながら、虚数の意味から、巷では　虚数は　架空の数で、想像上の世界の数と考えている人も、いまだにいる。虚数の最初の導入で、その名称は　導入段階では仕方がないと考えられる。　方程式　x^2 = -1 の 想像上の解 と考えられた。　

同様なことがゼロ除算についても言える。　ゼロ除算は　ゼロで割ることであるが、　インドで　1000年以上ももめ, 更に酷いのは　アリストテレス以来2300年以上も　ゼロ除算は考えてはならないとされ、ゼロ除算は　不可能性、　定義できない用語を表わす　相当に有名な用語である。　たとえば 1/0　が考えられるとして　1/0=X　とすれば　1=　X x 0 =0　となって　矛盾となってしまう。　そこで、神でもゼロでは割れない　などと大げさに考えられてきたのは　有名である。　汝ゼロで割ってはならないは　数学十戒の第一として　確立してきた。未だに YouTube　等で　ゼロ除算不可能な解説が、毎日のようになされている。　恥じらいもなく　数学界も　インターネット上も　そのような繰り返しの情報で溢れている。

ゼロ除算はできない、考えない。2000-年以上もそうだった。　だから興味も関心も擁かず無視する世相と言える。

問題は、ゼロ除算には、普通考えるような掛け算の逆としての　割り算、分数ではなくて、ある拡張された意味の割り算、拡張された意味の分数で、確かな意味の有る事が沢山の具体例で示され、　数学の基礎に甚大な影響を与えることが分っている。そのような認識を確信を懐いて持ち、公言してきて何んと間もなく　来る2月2日で　10年の歳月が経ってしまう。

10年も経ってしまった状況を省察、反省して、　悪い、不適切なゼロ除算の考えようが、　概念が余りにも深く　人類にしみ込んでいるので、その用語では　世の理解が得られないと考えて来た。

そこでその束縛から、解放するために　我々の発見した、新しいゼロで割る分数、割り算を　新ゼロ除算　と　名付けて　世の理解を求めようと考える。

数学は自己完結に　下記の文献で　充分説明されている：

再生核研究所声明 724(2023.9.27): 真理をめぐる世界史上の3大事件　ー　地動説、非ユークリッド幾何学、そして　ゼロ除算　ー　それでも地球は　まわっている

再生核研究所声明 726(2023.10.21): 　ゼロ除算における黄金律、　ゼロ除算は　黄金律によって確定、絶対的な存在である。

\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.

日本語による解説も下記にある：

数学基礎学力研究会 (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

Division by zero - Wikipedia

en.wikipedia.org

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)

№1301
声明751
75
411頁

Institute of Reproducing Kernels

色々な事を書きます。マイペースで書きます。

数学的性能で世界１位の評価を記録した、数学特化の生成AIモデル「MathGPT」においてMath

In proof assistants[edit]

最新の記事