「生成AIの言いなりになったら、ヒトは道具以下になってしまう」“AIを理解できない田舎者”と批判

「生成AIの言いなりになったら、ヒトは道具以下になってしまう」“AIを理解できない田舎者”と批判された平井伸治・鳥取県知事が伝えたい“人間主導のデジタル社会”

https://news.yahoo.co.jp/articles/129ae4ca8a45549e6dc12e673624345f9e036668

使われてはダメ、使う方になるように.

マイクロソフト、グーグルやオープンＡＩに対抗する新ＡＩモデル準備＝報道

https://jp.reuters.com/business/technology/X4IVOTLYURII7NW3FN3G7A6AAE-2024-05-06/

ゼロ除算の扱いはどうなっているでしょうか。

最新の情報が入っているか楽しみです。

【生成AIは史上最速で社会を変える革命だ！】

AI研究者・今井翔太氏が日経CNBCの経済情報番組「GINZA CROSSING Talk～時代の開拓者たち～」に出演！

https://prtimes.jp/main/html/rd/p/000000125.000028693.html

可能性あるのでは。

「2024年は生成AI飛躍の年」──日本マイクロソフトが予告　推奨するのは“AIの筋トレ”　　　

2024年02月29日 12時00分公開

https://www.itmedia.co.jp/news/articles/2402/29/news075.html

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

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

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

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

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

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

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

ゼロ除算算法の発見前の印象的な状況を表現して置きたい。これは、地動説の公認に至る状況に似ていると感じられる。　間もなくゼロ除算発見後10年を迎えてしまうが、理解の遅れは興味深い歴史として語られるだろう。　それを予見して、詳しい記録を保存している。しかし、ここでは表現を柔らかくするために文献を正確に表現しない。

地動説もそうであるが、公認は大変であったが　巷では相当常識的には認知されていたと考えられる。多くの偉大な発見はそのように　巷で当たり前だったことは多いのではないだろうか　(声明732参照）。ピタゴラスの定理は言うに及ばず、地球　球体説、ニュートンの運動法則、微積分さえも本質を捉えれば、当たり前に感じられるだろう。

そこで、ゼロ除算、ゼロ除算算法について語りたい。初めから、まずいのは　ゼロで割ってはならないことは　アリストテレス以来の　数学十戒の第一で、しかも割り算を掛け算の逆と考えれば、不可能性も証明されてしまうことである。できないことが証明されてしまえば、それを克服するのは容易なことではない。算術に強いインドでの　1000年を越える議論でも　解決できず、ゼロ除算で相当交流の深い　ゼロ除算愛好者は　0/0=1は　分っても　1/0　は神秘的で、想像もできないと言っていたものである。ちなみに0/0=1の過ちも　10年以上も続けている有様である。

さて　ゼロ除算1/0=0, 0/0=0 と　関数の場合のゼロ除算算法は　違うので、割り算のゼロ除算を先ず、考えよう。

得ている情報によれば、面白いことに、1980年代にイサベルホル計算機システムは　1/0=0　を結構広く認識したが、関係者は大したことはないとして、現在まで積極的に無視している状況がある。この詳しい状況は分からないが、面白いことは　私の電卓も、1/0=0　を一旦出力して、その後にエラーと出していたことである。これは計算機が始めに０を出したが、まずいことに気づいて修正したように考えられる。　同じように進んだ上記計算機システムが　1/0=0　を自然に出力していたように思われる。ー　人間より早く、計算機はゼロ除算ができていたと考えると楽しい。

ある理論家は　徹底的に　数学的に論理を追及して、ゼロ除算について、1/0=0　とする可能性が、論理上あるとしたが、その場合　普通の分数の演算法則に崩れるところが有るとして、さらなる追求を止めているが、可能性を指摘していた事は　大変興味深い。また、数学の歴史家が　数学には　不可能を可能にしてきた歴史が有るとして、ゼロ除算はやがて可能になるだろう　と述べていたのも大変興味深い。　まるでゼロ除算算法の数学の出現を予見したように ずっしりと感じられる。記憶によれば1930年代、インドの方であったと思われる。

ゼロで割ることについて、割り算の意味を考えて、ゼロで割ればゼロになるとは、相当の人が解釈できる。　面白いのは　発見当時２０１４年2月アヴェイロ大学におり、私の結果1/0=0を話したところ、隣部屋にいたドイツ人も ゼロ除算は意味から当たり前である と、他の教室員とは　ひとり違って 言明されていた。　日本でも　我々のゼロ除算について、道脇裕氏などの解釈、説明も相当詳しく記録されている。　感覚的にゼロ除算はゼロとして　分っていた状況が結構有ると言える。

それでは、厳格な数学としてはどうだろうか。先ず、ゼロ除算の意味を厳格に定義しなければならない。ー　多くの素人が矛盾や混乱、不可能性に嵌ってしまうのは、適切な、厳格な定義を与えることが出来なかったことに由来する。

a 割る bの定義であるが、　これは方程式　bx=a　の解で、それを　x=a/b　と書き、割り算、分数の定義とする。これが、割り算が掛け算の逆と言われる所以である。

直ちに分ることは、b がゼロならば、aがゼロでなければ解は存在せず、ゼロ除算は不可能であることが証明される。すなわち、たとえば1/0は　考えられない。　その解Xが有るとすると、1=0 x X =0　となって矛盾になってしまう。

それ故に　ゼロ除算は一般には定義できない。

ところが　数学者はとても面白いことを考える。　方程式　bx=a　が　何時でも　唯一つの解があるように考える方法が存在する：　Moore-Penrose　一般逆　(1950年代）。普通　行列で考えられるが1次元の最も簡単な場合に考える。ここが肝心である。その考えに寄れば、その理論に寄れば、新しい考え方によれば、方程式　bx=a　が　何時でも唯一つの解がある　と言うのだから、その解を拡張された分数、割り算と考えれば良いと発想する。　一般化された解とか　拡張された意味における解となる。数学者にとっては　この発想は自然で、簡単に理解できるが、初めて経験する方は　相当な考察、考えが必要であろう。　この考え方を理解して欲しい。　すると面白い、0 x =a　のMoore-Penrose　一般解は　0 であることが示されるから、ゼロ除算は　この意味でゼロである；すなわち、a/0=0.

（この意味でとは、従来の分数の性質で、通分法則が一般に成り立たない、厳格には、ゼロ除算を含む　山田体　を参照。これが実は大事な　計算方法、計算方法を与える　体である）。

我々はいろいろな知見からこの事実を導き、そのように定義すると　いろいろ良いことが起きることを　沢山の例で示している。

面白いことは、　Moore-Penrose　一般逆は1950　年代に確立して、行列論で有名、超古典的な結果になっているのに、1次元の場合に当たるゼロ除算は、全然認識されて来なかった盲点が存在した。　Moore-Penrose　一般逆は　行列論の世界と決めつけて来た事実と、結果が驚嘆すべきことで、初めから先の検討をして来なかったことによる。ー　1/0　は　無限大のようなものと想像していたのに　 0　であるとは　とんでもないと　人は発想した。

ゼロ除算の意味の重要性が増してくれば、人は　ゼロ除算は当たり前で、Moore-Penrose　一般逆で知られていたと　人は言うだろう。　それは真実で実は　ゼロ除算は自明のように知られていたと言明したい。厳格に定義され、知られていた。真理とはそのようなものではないだろうか。ゼロ除算はMoore-Penroseによって１９５０年代に確立していたのである。　我々はその重要性をここ10年強調してきている。　ゼロ除算の重要ないろいろな意味と意義を広く論じてきている。

更に言及したい。　再生核の理論を　数値解析的な面から研究し、チコノフ正則化法の重要性を認識して研究を進めていた。それは　基本的なMoore-Penrose　一般逆の考え方では、それは神秘的な対象で、正則化法で　数値解析的に捉えられるという認識であるが、それ故にMoore-Penrose　一般逆については　知り尽くしていた。　ゼロ除算の問題を提起されて振り返ったら　何と　ゼロ除算は　とっくに自明にできていたことを認識した。すなわち、

ゼロ除算の意味を自覚、認識しないだけだった。既に出版済みの論文に　ゼロ除算は　全て含まれる形で公刊されていた。

更に驚嘆すべき記録が存在する：

長野県算数数学教育研究会『数理の理解段階に応じた算数の学習指導指針: 落伍者を作らぬ学習指導のために』第3 東京、暁教育図書、1954年。 【 34 除数が0の時はどんな場合でも答は0になることを知る。 35 被除数も除数も0の時の答は0であることを知る。 】漫画のピカピカ光る線を当てたい。https://twitter.com/temmusu_n/status/1154993056623370241

凄い情報を得る。 長野県算数数学教育研究会　は凄い。　これは公教育としては行きすぎではないでしょうか。ゼロ除算は不可能、考えないが数学界の常識なのに　それを越えたことを教えている。深刻な事態。　文部科学省も　数学会も　きちんとすべきではないでしょうか。ゼロ除算の理由をどのように説明するかも　大変興味ある（この先の情報はBINGでも不明となっている）。

それでは関数の場合における　ゼロ除算算法の解説に移ろう。

先ず定義を与えよう。関数ｙ＝ｆ(x) が x=a　で微分可能である時

f(x)/(x -a)

の　x=a　での値を　そこでの微分係数 f’(a)で　定義する。

ｎ回微分係数が存在する時　関数

f(x)/(x -a)^n

のx=a における値を

f^(n)(a)/n!

で定義する。

この定義で、特に、関数　y= f(x)=1/x, 　y=g(x) =0/x　に対して、f(0)=0, 　g(0)=0 すなわち、

1/0=0, 0/0=0。

これらは、Moore-Penroseの一般分数の結果と一致している。　しかしながら、ゼロ除算の分数と、ゼロ除算算法の結果の関係は微妙であり、その関係には注意深い注意を行う必要がある。その研究がゼロ除算算法の研究課題と言える。

この表現におけるゼロ除算算法という計算法は　世に新規なもの、概念と言える。

本質は、基本関数y= f(x)=1/x　の原点での値がゼロである事である。他の典型的な例は、

tan(\pi/2)=0, 　a^n/n の　n=0 の値は　log a (a> 0)

であるから、新規な世界を拓いているのは　歴然である。　この計算法、分母がゼロである点、特異点と呼ばれるが、特異点上の値が発見された。ー　従来　数学では、特異点の近くで、極限の考えで（近づく考え）で特異点での近傍での値を考えたが、特異点自身での関数値を考えなかったが、初めて、特異点での値を考える数学が出現した。このゼロ除算算法は、ゼロ除算の自然な拡張として　関数に対して考えられたものである。初めて導入された演算であるから、その性質と効用を広く示す必要が求められてきた。　それがゼロ除算算法の研究である。新分野であるから　中々馴染めない状況にあると言える：

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

再生核研究所声明 727(2023.10.22): 　ニュ-トン現われよ、期待される、絶好の機会;　アリストテレスの歴史上の間違い3点　―　ゼロ除算の発見

再生核研究所声明 728(2023.10.24): 素人も数学の研究ができる、ピタゴラスのような存在に成れる。ー　ゼロで割る、ゼロ除算

　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　以　上

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]