Index / Reload / Edit
リンク先のページで、「transfinite number」に「超越数」って訳語をあてているのも、ちょっと気になりますね。
修正後の連続体仮説のページや他の数学関連のページについてもいろいろ言いたいことはあるのですが、一番の問題点を直して頂けたので、今回はこれで良かったのではないかと思います。「コンピューターで厳密な証明」という考えをお持ちですので、教育関連のページももう少し正確に分かりやすく記載して頂きたいという気持ちはあります。
てなさくさんの次の指摘に、私も一票。＞「transfinite number」に「超越数」って訳語
たしかに気持ちが良くはないのですが、余りしつこく訂正依頼というわけにもいきません。私自身はひとまずこの話題に関しては終息させたいと思います。
要するに中村氏がアレフ１の定義を誤解してただけのように思う。
「コンピューターで厳密チェック」というのは、別にトンデモでもなんでもない。もちろん「厳密」というのは、結局「文字面」ということでしかなく、本来の正しさ云々は、形式化の外に漏れだしてしまうということはあるにしても、だ。
＞「transfinite number」に「超越数」って訳語をあてているのも、ちょっと気になりますね。まあ、知らない上に調べないんでしょうね。別に遠慮する必要ないでしょう。「日本ではこれは超限順序数って呼ばれてますよ」というだけのことですから。ついでに「どうせなら、１０件指摘したらなんかいただけるとかないですかね？ クヌースはそうしてるみたいですけど」とちゃっかり言ってみるとか。ただムカつくだけだと、自分の脳ミソぶっ壊すだけですよ。いや、ほんと、マジな話。
たしかに単純な勘違いと言えないこともないのですが、やはり大学のページで発信されているのはいろいろ弊害があるかなと思いました。コンピューターでの証明過程の検証に関しては、人間のミスを補完するという意味ではそれなり有意義なのかなとは思います。ただし現状では検証に対する手間がかかりすぎるのは間違いないと思います。それから数学はやはり人間の頭脳で、という思い込みもあると思います。今回の訂正で過去の「トンデモ」という題名も消してしまいたかったのですが、書いてしまったという事実はありますので、そこのところは修正しませんでした。今回の記事ではその辺り言い分けがましくなってしまったかも知れません。私自身 (一般) 連続体仮説について非常な愛着と、相反するかも知れませんが、恐れに近い感情を持っていますので、あまりいい加減なことを書いて欲しくかなったので、他の部分について「脳ミソぶっ壊す」ことはないと思います。といいますか、親しい人以外に誤りを指摘するとなると、それなり文面を考えたり存外面倒なので、これ以上どうでもいいやというのが本音です。
皆が皆、自分と同様の思い入れを共有してるわけじゃないので、そういう人は「縁無き衆生」だと思うのが、よろしいですよ。「コンピュータによる証明」について、「人よりコンピュータのほうが確かだ」とかいうのは、実は全然当たってないので、その点についてはいくらでも文句をいうべきかと思いますが、手間云々というのは、むしろ研究の励みであって、意欲を失わせるものではない気がします。（学問は所詮マゾヒストの趣味ですよ）
私は、いまだに連続体仮説の何が重要なのかわかりません。非決定的だと聞いてますますそう思いました（ｗ。コーエンはよくやったと思いますが。
それこそ思い入れというものですよ。
＞「数学の論文はコンピューター可読な形式とし証明のチェッカーを通す」ことが実質義務づけられたりすると、とてもいやな未来が待っているような気がします。それはないでしょう。というか、実際には、コンピュータが自分で穴埋めでもなんでもしやがれ、ってことにならないと使えないでしょう。人間様は忙しいんですよｗ＞優秀な人はやはり現在のような自然言語で論文を書くと思います。優秀な人は、そもそも自然言語がニガテです（ｗ。どこの数学科でも優秀な人に限って、コトバがヘンだったりしますし、実際コトバで考えてないですから。彼等にとって自然言語で書くこと自体もう十分苦痛でしょう（ｗ＞どんどん湧き出るイマジネーションをコンピューターの言語に翻訳している様なつまらないことをする動機も暇もないからです。まあ、これは人によるので、なんとも言えません。＞その場合一番犠牲になりそうなのは、普通の学部生や大学院生で、元の論文をコンピューター語に書き直し、つまらない誤りを修正したり、どうでも良い細部を埋め込む人海戦術にかり出されるのではと危惧するのです。それはないですよ。数学はチームワークじゃないから。数学の先生は、学生なんて手足だと思ってないし、思ったところで手足として使うだけの才覚はないし。そもそも自分ひとりで考えればいいとおもって数学者になったような人たちばっかりですから。＞現に今の生物学など一部その様な状況になっていると思うのですが。生物学は数学とは全然違いますよ。あれはガッチリと徒弟制度ですから。＞コンピューターによる証明の検証という代物は、運用を誤ると学生を先生の下働き要員に使うようなシステムになるような気がして、どうしても好きになれないのです。なりようがないと思いますよ。考えるのは先生本人だから。＞上のJordanの定理の「業績」においてすでに犠牲者が出ていなければ良いのですが。そもそも、数学したい人は、あそこの研究室にいかないから「犠牲者」はいないでしょうｗ。機械証明の場合、新しい定理を証明するとかいうのはまずないでしょう。要は数学の形式化ってことです。数学そのものの創造とは別に、そういうことに興味をもつ人がいてもよろしいかとは思います。形式化それ自体にバグが混入する可能性は多々あるから「形式的証明のほうが信頼できる」とはいえないでしょうが、そのことは、形式化そのものの意義を失わせるわけではない。やりたい人がやる分には結構なことだと思います。
中村氏は、数学というより情報数学なのでしょう。情報数学は数学とは違います。物理学に対する工学のようなものでしょうか。コンピュータ至上主義に陥りやすいのも分かるような気がします。情報数学では、ががみさんの危惧が現実となっていても不思議はないように思えます。数学は、まず疑うことから始まりますので(？)、というか、自分で納得しないことには始まらないので、情報数学とは相反する学問ではないでしょうか。尤も、コンピュータがエレガントな証明をしてくれれば、考えも変わりますが。
(通りすがりさん) 昔の記事は感情的になり無理やり批判的な理屈を考え出した面はあると思います。若かったのですよ (笑)。 あの辺りは削除してもよいのですが、前にも書いたように「書いてしまった」という事実はありますので、証拠は残しておいたほうが良いかなと考えたのです。優秀な人が自然言語が苦手ということはどうでしょうか。少なくとも私が知る範囲の優秀な方々はみな自然言語についてもとても堪能だと思いますが。
(Joe☆さん) こんにちは。どうもおひさしぶりです。中村氏は情報数学というより、数学とは全く無縁の方だと思います。数学の定理に対して、コンピューターでの検証 (これ自体は原理的にそれなり信頼できます) を通さないと全く信用しないというお立場のようですから。それに関しては本文での信州大学連続体仮説に対するリンク先での、最後の方の文面が如実に物語っていると思います。私は全然詳しくないのですが、最近はいわゆる情報系と数学の基礎的な部分に関してかなり接近した分野もあるようです。ただし数学を実体験していない情報系一部の人で非常に優秀な方であるにもかかわらず「ちょっと数学に対する考えがずれているな」と感じる場合があることは事実です。もちろん皆がそうであるという意味ではありません。コンピューターが自律的にエレガントな証明を行うことは永久にないと思います。最近ご無沙汰していて申しわけありません。一度お会いする機会があるとうれしいです。ではでは。
中村八束氏は数学科の出身ですね。http://markun.cs.shinshu-u.ac.jp/kiso/staff/nakamura/index-j.html数学の形式化に興味をもつ人がいても悪くないと思いますよ。このあたりのことについては、萩谷昌己さんが自嘲的（？）に語ってます。http://nicosia.is.s.u-tokyo.ac.jp/pub/essay/hagiya/essay/keishikikaもちろん、「形式化すればそれだけでミスがなくなる」という発想は実は正しくなくて、形式化自体のミスを考える必要があります。これは形式化されたものだけ見ても見つかりません。V&Vでいえば、verifyだけじゃなくてvalidateが必要ということです。
＞優秀な人が自然言語が苦手ということはどうでしょうか。＞少なくとも私が知る範囲の優秀な方々はみな自然言語についてもとても堪能だと思いますが。数学者のアダマールの著書に「数学における発明の心理」（発見、でないところが面白い）というのがあって、その中に、アダマールのアンケートに対するアインシュタインの回答というのがあるのだが、そこでアインシュタインは「言語では考えない」と、はっきり述べている。
＞コンピューターでの検証を通さないと全く信用しないというか、正しさの根拠を「形式」に求めているのでしょう。私自身は、コンピュータがエレガントな証明を行う必要性を爪の垢ほども感じていません。むしろ、エレガントな証明などありそうもないものをバカ力でねじ伏せるために、コンピュータを使うのが「リコウ」なやり方でしょう。
あれれっ、失礼しました。確かに中村氏は「数学科」出身ですね。でも私が考える数学とは無縁な方だと思います。もっともそれは個人の好みですからどうでもよいですが。それから天才的な数学者が言語で思考しないらしいことは知っていました。ただ、そのような天才も、通常の言語に関し極めて堪能な場合が多いので、全く根拠はないのですが、その思考自体は言語が進化した形式なのかも知れません。数学の形式化が厳密性以外の部分でも極めて重要なことは分かります。今回の場合、形式化という行為が計算機という物理的な実体と関連する理由がよく分からないのです。
＞形式化という行為が計算機という物理的な実体と関連する理由がよく分からないのです。数学という行為が数学者（およびその脳味噌）という物理的な実体と関連する理由が分からないのと同じですよｗ
単なる個人の感情なのですが、要は数学に計算機が介入するのが嫌いなんですよww
要は、「脳は、計算機とは全然違う！」という人間至上主義がいかがわしいと思ってるだけで（ｗ。実は計算機にもクオリアってあるんじゃないかと思わずにいられない今日この頃。とはいえ、魂のデジタル化への道はあまりに遠い（ｗ。
私が計算機を余り好まないと同様に、計算機にも嫌われているようです。そういう意味でのクオリアあるかも。初期状態では 10行ごとに必ずコンパイルエラーもしくはバグがでる orz
リンク先のページで、「transfinite number」に「超越数」って訳語をあてているのも、ちょっと気になりますね。
修正後の連続体仮説のページや他の数学関連のページについてもいろいろ言いたいことはあるのですが、一番の問題点を直して頂けたので、今回はこれで良かったのではないかと思います。「コンピューターで厳密な証明」という考えをお持ちですので、教育関連のページももう少し正確に分かりやすく記載して頂きたいという気持ちはあります。
てなさくさんの次の指摘に、私も一票。
＞「transfinite number」に「超越数」って訳語
たしかに気持ちが良くはないのですが、余りしつこく訂正依頼というわけにもいきません。私自身はひとまずこの話題に関しては終息させたいと思います。
要するに中村氏がアレフ１の定義を誤解してただけのように思う。
「コンピューターで厳密チェック」というのは、別にトンデモでもなんでもない。もちろん「厳密」というのは、結局「文字面」ということでしかなく、本来の正しさ云々は、形式化の外に漏れだしてしまうということはあるにしても、だ。
＞「transfinite number」に「超越数」って訳語をあてているのも、ちょっと気になりますね。
まあ、知らない上に調べないんでしょうね。
別に遠慮する必要ないでしょう。
「日本ではこれは超限順序数って呼ばれてますよ」
というだけのことですから。
ついでに
「どうせなら、１０件指摘したらなんかいただけるとかないですかね？
クヌースはそうしてるみたいですけど」
とちゃっかり言ってみるとか。
ただムカつくだけだと、自分の脳ミソぶっ壊すだけですよ。
いや、ほんと、マジな話。
たしかに単純な勘違いと言えないこともないのですが、やはり大学のページで発信されているのはいろいろ弊害があるかなと思いました。コンピューターでの証明過程の検証に関しては、人間のミスを補完するという意味ではそれなり有意義なのかなとは思います。ただし現状では検証に対する手間がかかりすぎるのは間違いないと思います。それから数学はやはり人間の頭脳で、という思い込みもあると思います。今回の訂正で過去の「トンデモ」という題名も消してしまいたかったのですが、書いてしまったという事実はありますので、そこのところは修正しませんでした。今回の記事ではその辺り言い分けがましくなってしまったかも知れません。
私自身 (一般) 連続体仮説について非常な愛着と、相反するかも知れませんが、恐れに近い感情を持っていますので、あまりいい加減なことを書いて欲しくかなったので、他の部分について「脳ミソぶっ壊す」ことはないと思います。といいますか、親しい人以外に誤りを指摘するとなると、それなり文面を考えたり存外面倒なので、これ以上どうでもいいやというのが本音です。
皆が皆、自分と同様の思い入れを共有してるわけじゃないので、そういう人は「縁無き衆生」だと思うのが、よろしいですよ。
「コンピュータによる証明」について、「人よりコンピュータのほうが確かだ」とかいうのは、実は全然当たってないので、その点についてはいくらでも文句をいうべきかと思いますが、手間云々というのは、むしろ研究の励みであって、意欲を失わせるものではない気がします。（学問は所詮マゾヒストの趣味ですよ）
私は、いまだに連続体仮説の何が重要なのかわかりません。非決定的だと聞いてますますそう思いました（ｗ。コーエンはよくやったと思いますが。
それこそ思い入れというものですよ。
＞「数学の論文はコンピューター可読な形式とし証明のチェッカーを通す」ことが実質義務づけられたりすると、とてもいやな未来が待っているような気がします。
それはないでしょう。というか、実際には、コンピュータが自分で穴埋めでもなんでもしやがれ、ってことにならないと使えないでしょう。人間様は忙しいんですよｗ
＞優秀な人はやはり現在のような自然言語で論文を書くと思います。
優秀な人は、そもそも自然言語がニガテです（ｗ。どこの数学科でも優秀な人に限って、コトバがヘンだったりしますし、実際コトバで考えてないですから。彼等にとって自然言語で書くこと自体もう十分苦痛でしょう（ｗ
＞どんどん湧き出るイマジネーションをコンピューターの言語に翻訳している様なつまらないことをする動機も暇もないからです。
まあ、これは人によるので、なんとも言えません。
＞その場合一番犠牲になりそうなのは、普通の学部生や大学院生で、元の論文をコンピューター語に書き直し、つまらない誤りを修正したり、どうでも良い細部を埋め込む人海戦術にかり出されるのではと危惧するのです。
それはないですよ。数学はチームワークじゃないから。
数学の先生は、学生なんて手足だと思ってないし、思ったところで手足として使うだけの才覚はないし。そもそも自分ひとりで考えればいいとおもって数学者になったような人たちばっかりですから。
＞現に今の生物学など一部その様な状況になっていると思うのですが。
生物学は数学とは全然違いますよ。あれはガッチリと徒弟制度ですから。
＞コンピューターによる証明の検証という代物は、運用を誤ると学生を先生の下働き要員に使うようなシステムになるような気がして、どうしても好きになれないのです。
なりようがないと思いますよ。考えるのは先生本人だから。
＞上のJordanの定理の「業績」においてすでに犠牲者が出ていなければ良いのですが。
そもそも、数学したい人は、あそこの研究室にいかないから「犠牲者」はいないでしょうｗ。
機械証明の場合、新しい定理を証明するとかいうのはまずないでしょう。要は数学の形式化ってことです。数学そのものの創造とは別に、そういうことに興味をもつ人がいてもよろしいかとは思います。形式化それ自体にバグが混入する可能性は多々あるから「形式的証明のほうが信頼できる」とはいえないでしょうが、そのことは、形式化そのものの意義を失わせるわけではない。やりたい人がやる分には結構なことだと思います。
中村氏は、数学というより情報数学なのでしょう。
情報数学は数学とは違います。
物理学に対する工学のようなものでしょうか。
コンピュータ至上主義に陥りやすいのも分かるような気がします。
情報数学では、ががみさんの危惧が現実となっていても不思議はないように思えます。
数学は、まず疑うことから始まりますので(？)、というか、自分で納得しないことには始まらないので、情報数学とは相反する学問ではないでしょうか。
尤も、コンピュータがエレガントな証明をしてくれれば、考えも変わりますが。
(通りすがりさん) 昔の記事は感情的になり無理やり批判的な理屈を考え出した面はあると思います。若かったのですよ (笑)。 あの辺りは削除してもよいのですが、前にも書いたように「書いてしまった」という事実はありますので、証拠は残しておいたほうが良いかなと考えたのです。
優秀な人が自然言語が苦手ということはどうでしょうか。少なくとも私が知る範囲の優秀な方々はみな自然言語についてもとても堪能だと思いますが。
(Joe☆さん) こんにちは。どうもおひさしぶりです。
中村氏は情報数学というより、数学とは全く無縁の方だと思います。数学の定理に対して、コンピューターでの検証 (これ自体は原理的にそれなり信頼できます) を通さないと全く信用しないというお立場のようですから。それに関しては本文での信州大学連続体仮説に対するリンク先での、最後の方の文面が如実に物語っていると思います。
私は全然詳しくないのですが、最近はいわゆる情報系と数学の基礎的な部分に関してかなり接近した分野もあるようです。ただし数学を実体験していない情報系一部の人で非常に優秀な方であるにもかかわらず「ちょっと数学に対する考えがずれているな」と感じる場合があることは事実です。もちろん皆がそうであるという意味ではありません。
コンピューターが自律的にエレガントな証明を行うことは永久にないと思います。
最近ご無沙汰していて申しわけありません。一度お会いする機会があるとうれしいです。ではでは。
中村八束氏は数学科の出身ですね。
http://markun.cs.shinshu-u.ac.jp/kiso/staff/nakamura/index-j.html
数学の形式化に興味をもつ人がいても悪くないと思いますよ。
このあたりのことについては、萩谷昌己さんが自嘲的（？）に語ってます。
http://nicosia.is.s.u-tokyo.ac.jp/pub/essay/hagiya/essay/keishikika
もちろん、「形式化すればそれだけでミスがなくなる」という発想は実は正しくなくて、形式化自体のミスを考える必要があります。これは形式化されたものだけ見ても見つかりません。V&Vでいえば、verifyだけじゃなくてvalidateが必要ということです。
＞優秀な人が自然言語が苦手ということはどうでしょうか。
＞少なくとも私が知る範囲の優秀な方々はみな自然言語についてもとても堪能だと思いますが。
数学者のアダマールの著書に「数学における発明の心理」（発見、でないところが面白い）というのがあって、その中に、アダマールのアンケートに対するアインシュタインの回答というのがあるのだが、そこでアインシュタインは「言語では考えない」と、はっきり述べている。
＞コンピューターでの検証を通さないと全く信用しない
というか、正しさの根拠を「形式」に求めているのでしょう。
私自身は、コンピュータがエレガントな証明を行う必要性を爪の垢ほども感じていません。むしろ、エレガントな証明などありそうもないものをバカ力でねじ伏せるために、コンピュータを使うのが「リコウ」なやり方でしょう。
あれれっ、失礼しました。確かに中村氏は「数学科」出身ですね。でも私が考える数学とは無縁な方だと思います。もっともそれは個人の好みですからどうでもよいですが。
それから天才的な数学者が言語で思考しないらしいことは知っていました。ただ、そのような天才も、通常の言語に関し極めて堪能な場合が多いので、全く根拠はないのですが、その思考自体は言語が進化した形式なのかも知れません。
数学の形式化が厳密性以外の部分でも極めて重要なことは分かります。今回の場合、形式化という行為が計算機という物理的な実体と関連する理由がよく分からないのです。
＞形式化という行為が計算機という物理的な実体と関連する理由がよく分からないのです。
数学という行為が数学者（およびその脳味噌）という物理的な実体と関連する理由が分からないのと同じですよｗ
単なる個人の感情なのですが、要は数学に計算機が介入するのが嫌いなんですよww
要は、「脳は、計算機とは全然違う！」という人間至上主義がいかがわしいと思ってるだけで（ｗ。実は計算機にもクオリアってあるんじゃないかと思わずにいられない今日この頃。とはいえ、魂のデジタル化への道はあまりに遠い（ｗ。
私が計算機を余り好まないと同様に、計算機にも嫌われているようです。そういう意味でのクオリアあるかも。初期状態では 10行ごとに必ずコンパイルエラーもしくはバグがでる orz