「有名な数学者も間違える」-- Grothendiek, Lawvere and Voevodsky
難しい論文を、ウンウンわかったつもりになって読み進んでいたら、途中で「なんちゃって」とか「うそピョーン」とか書かれていれば、やる気は失せるだろう。
1983年のグロタンディックの仕事 ‘Pursuing Stacks’ は、ある分野（presheaf Topos）のホモトピー論について、非常に多くの問題を論じている。それは、600ページもある。グロタンディックは、数週間にわたって、夜通しタイプライターに向かっていたと思う。
グロタンディックだって、疲れがたまれば間違いを犯す。朝になると、グロタンディックは、前夜に行った証明・説明の誤りに気づく。ただ、彼は、前夜の間違いを草稿から消そうとせず、それはそのままにして、訂正された証明・説明を朝には草稿に付け加えて、仕事を続けたのだ。
グロタンディックのこの草稿を、どのような形で世に出すべきかで、ローヴェールとグロタンディックで意見の違いが起きてしまう。ローヴェールは、良心的な編者としては、間違った部分は削除し、それについては編者のコメントをつけて出すべきだと言ったのだが、グロタンディックは、草稿の間違いをそのまま残すことに固執した。
その理由が面白い。
「そうすれば、学生たちに、有名な数学者でさえ間違いを犯すということを学ばせるいい機会を提供することになる。」
ローヴェールは反対する。学生に提供すべきは、そんなことではなく、この本をちゃんと学生たちに読んでもらう機会を作ること。科学的な対象は、それでなくとも学ぶのが難しいのに、罰ゲームみたいな回り道を学生にさせる必要はないと、譲らない。
両者の議論は平行線で（そういえば、二人とも頑固そう）、結局、ローヴェールが編者になって、グロタンディックの‘Pursuing Stacks’ を出版するという世紀のプロジェクトは幻に終わった。
（僕が、そうした試みがあったことに、ようやく気づいたのは、今年の夏だった。もっとも、2013年のローヴェールの発言 "FAREWELL TO AURELIO" http://www.acsu.buffalo.edu/~wlawvere/FarewellAurelio.htm
まで、そのことを知っていた人は、ほとんどいなかったはずだ。）
ただ、無茶振りをしているかに見える、グロタンディックの「数学者も間違える」ものだという認識は、大事なものだと思う。それは、ヴォヴォドスキーの大きな関心の一つだった。それについては、以前にもここで触れたことがある。（「Voevodsky と証明支援システム UniMath」https://maruyama097.blogspot.com/2017/11/voedvodsky-unimath.html )
同じ関心を持ちながら、グロタンディックとヴォヴォドスキーでは、解決の方向が違っている。グロタンディックは、学習者が誤りに気付いて、そこから教訓を学び、さらに賢くなることを期待している。ヴォヴォドスキーは、問題が複雑になるにつれて、人間には誤りに気づくのが困難になり、数学の「累積的知」という性格上、誤りが蓄積・拡大することに危機感を持っている。だから、人間ではなく、コンピュータによる証明チェックが不可欠だと。
「数学者も間違える」問題は、見かけ以上に、深い広がりを持った問題なのだ。（少なくとも、人工知能研究とは重要な接点を持つ（はずである））。それについては、別の機会に触れるとして、ここでは、Stacks Theory の現在の姿を紹介したい。
ヴォヴォドスキーは、GitHubを使って集合知として数学の教科書を書くことを始めたのだが（ "The HoTT Book: Homotopy Type Theory" https://homotopytypetheory.org/book/ ）、こうしたスタイルがもっとも進んでいるのが、実は、この分野なのである。
The Stacks Project というプロジェクトがある。https://stacks.math.columbia.edu/ 280人以上の数学者が参加して、書かれた教科書は 6000ページを超えている！ https://stacks.math.columbia.edu/browse （ディープ・ラーニングのカルパシーが、ふざけて、「数学論文」の「学習」に使ったのは、この6000ページだ。）明らかに、グロタンディックの時代とは、Stacks Theoryの情報の共有のスタイルとスピードは劇的に変化している。
ただ、「数学者も間違える」というのなら、たくさんの数学者が参加すればするほど、たくさんの間違いが生まれるはず。だから、実際、毎週のように、間違いは「訂正」されている。素晴らしい！
1983年のグロタンディックの仕事 ‘Pursuing Stacks’ は、ある分野（presheaf Topos）のホモトピー論について、非常に多くの問題を論じている。それは、600ページもある。グロタンディックは、数週間にわたって、夜通しタイプライターに向かっていたと思う。
グロタンディックだって、疲れがたまれば間違いを犯す。朝になると、グロタンディックは、前夜に行った証明・説明の誤りに気づく。ただ、彼は、前夜の間違いを草稿から消そうとせず、それはそのままにして、訂正された証明・説明を朝には草稿に付け加えて、仕事を続けたのだ。
グロタンディックのこの草稿を、どのような形で世に出すべきかで、ローヴェールとグロタンディックで意見の違いが起きてしまう。ローヴェールは、良心的な編者としては、間違った部分は削除し、それについては編者のコメントをつけて出すべきだと言ったのだが、グロタンディックは、草稿の間違いをそのまま残すことに固執した。
その理由が面白い。
「そうすれば、学生たちに、有名な数学者でさえ間違いを犯すということを学ばせるいい機会を提供することになる。」
ローヴェールは反対する。学生に提供すべきは、そんなことではなく、この本をちゃんと学生たちに読んでもらう機会を作ること。科学的な対象は、それでなくとも学ぶのが難しいのに、罰ゲームみたいな回り道を学生にさせる必要はないと、譲らない。
両者の議論は平行線で（そういえば、二人とも頑固そう）、結局、ローヴェールが編者になって、グロタンディックの‘Pursuing Stacks’ を出版するという世紀のプロジェクトは幻に終わった。
（僕が、そうした試みがあったことに、ようやく気づいたのは、今年の夏だった。もっとも、2013年のローヴェールの発言 "FAREWELL TO AURELIO" http://www.acsu.buffalo.edu/~wlawvere/FarewellAurelio.htm
まで、そのことを知っていた人は、ほとんどいなかったはずだ。）
ただ、無茶振りをしているかに見える、グロタンディックの「数学者も間違える」ものだという認識は、大事なものだと思う。それは、ヴォヴォドスキーの大きな関心の一つだった。それについては、以前にもここで触れたことがある。（「Voevodsky と証明支援システム UniMath」https://maruyama097.blogspot.com/2017/11/voedvodsky-unimath.html )
同じ関心を持ちながら、グロタンディックとヴォヴォドスキーでは、解決の方向が違っている。グロタンディックは、学習者が誤りに気付いて、そこから教訓を学び、さらに賢くなることを期待している。ヴォヴォドスキーは、問題が複雑になるにつれて、人間には誤りに気づくのが困難になり、数学の「累積的知」という性格上、誤りが蓄積・拡大することに危機感を持っている。だから、人間ではなく、コンピュータによる証明チェックが不可欠だと。
「数学者も間違える」問題は、見かけ以上に、深い広がりを持った問題なのだ。（少なくとも、人工知能研究とは重要な接点を持つ（はずである））。それについては、別の機会に触れるとして、ここでは、Stacks Theory の現在の姿を紹介したい。
ヴォヴォドスキーは、GitHubを使って集合知として数学の教科書を書くことを始めたのだが（ "The HoTT Book: Homotopy Type Theory" https://homotopytypetheory.org/book/ ）、こうしたスタイルがもっとも進んでいるのが、実は、この分野なのである。
The Stacks Project というプロジェクトがある。https://stacks.math.columbia.edu/ 280人以上の数学者が参加して、書かれた教科書は 6000ページを超えている！ https://stacks.math.columbia.edu/browse （ディープ・ラーニングのカルパシーが、ふざけて、「数学論文」の「学習」に使ったのは、この6000ページだ。）明らかに、グロタンディックの時代とは、Stacks Theoryの情報の共有のスタイルとスピードは劇的に変化している。
ただ、「数学者も間違える」というのなら、たくさんの数学者が参加すればするほど、たくさんの間違いが生まれるはず。だから、実際、毎週のように、間違いは「訂正」されている。素晴らしい！
素晴らしい？
コメント
コメントを投稿