再生核研究所声明 744（2024.1.26) 大きな証明検証システム達が ゼロ除算1/0=0/0=0 を保証している
これは ニュースを解説調で述べたい： 先ずメール：
|
From: |
Xena <comment-reply@wordpress.com> |
|
返信先: |
Xena <comment+ed083_jbv9l7glxtxu9n-40-k9f1jssyo367jw6a9xf67scrg@comment.wordpress.com> |
|
To: |
saburou.saitoh@gmail.com |
|
日付: |
2024/01/21 21:39 |
|
件名: |
[Xena] xenaproject commented on Division by zero in type theory: a FAQ |
|
送信元: |
b.wordpress.com |
|
署名元: |
wordpress.com |
で 次の事が知らされた：
New comment!
|
主要部は次のようである：
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年)
学術アドバイザー： リチャード・テイラー
我々はIsabelleがゼロ除算1/0=0/0=0 その他の我々の結果を保証している事実と関係情報をJose Manuel Rodriguez Caballero
から得ていたが 上記に Yes. So do Coq and Isabelle and many other theorem provers.
と相当信頼される数学者によって述べられていることが分かる。
Coqはフランスの、
Leanはアメリカの大きなソフト会社である。他にも多く有ると述べられている。それで、国際的な競争関係が激化しているようだ。 マル秘で適切な回答が得られない。
Isabelle はイギリスとドイツの連携の巨大なシステム。 １９８０年代から1/0=0を認識していたという。しかし関係者は永く無視して来た。
上記の彼らの分数 f(x,y) =x/y の定義と我々の拡張分数、 割り算の定義は 同じである。 我々は高橋の一意性定理によって動機付けや山田体の構成で そう宣言している。
Moore-Penrose一般解の考え方でも同じである。 それを元にゼロ除算算法に発展させて基本性質を導いている。上記検証は我々の理論を保証している。
沢山検証がなされているようである。
上記 Jose 氏と相当交流してきたが、何かマル秘、秘密対応に感じられ、多くの関係者にも交流を求めたが企業秘密の観を持ってきた。他のシステムも 公然と研究活動をしてきたのに 我々に連絡もしないで 開発を進めていた事実から、開発競争が激しく行われている様子が伺える。
次の事実も大事である：
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 が 論理、計算機システムの広範な確定的な保証を与えているばかりではなく、我々の展開しているゼロ除算算法の概念による研究が内々に進められている状況を示していると考えられる。
我々はゼロ除算発見の初期から ゼロ除算の発見が世界史に関わる問題であると認識して、その詳しい発展の経過を記録し、どんどん公開方式で展開、公表してきている。その内容を著書、論文に出版し、雑誌を創刊し、再生核研究所声明などでも公開している。
基本的な数学を無視続ける数学界に対して、絶えず数学界の対応の怠慢さを批判してきている。
以 上
２０２４．１．２５．９：０４ 一応纏める。
２０２４．１．２５．１０：０４ 確認。
２０２４．１．２５．１３：０２ 廊下の修繕を午前中にする。 寒いが良い天気。表現を吟味した。
２０２４．１．２５．１４：１０ 文を整える。
２０２４．１．２５．１５：４７ 良い。
２０２４．１．２５．１８：３０ 良い。
２０２４．１．２５．２１：４０ 良い。
２０２４．１．２６．５：５４ 良い、完成、公表。