Voevodskyの証明をDeep Learningは追えない。あるいは、黒板とチョーク。

30年近く、講義・講演はプロジェクターを使って来た。ビジュアルな情報があった方が、聴く方にもわかりやすいと思うし、話す方はデータが再利用できる。

でも、話せば伝わることとビジュアルな表現で伝えた方がいいこととの区別は、どこにあるのだろう？と考えたら、こんな例を思いついた。

図１は、先頃亡くなっらVoevodskyの証明の一部（だと思う）https://goo.gl/3y79Zb から。これを、口でしゃべったら、絶対うまく伝わらない。

（ただ、この例は、すごいのだ。僕は、カテゴリー論をちょっとかじったことがあるので二次元のdiagramなら、少しは追えるのだが、Voevodsky は、三次元で証明組み立てている！）

ただ、こうしたdiagramをプロジェクター用に、LaTexで組むのは大変なのだ。（もちろん、根性があればできるし、データは再利用できるのだが）

図２は、Deep LearningのKarpathyが、RNNを使って、Stacks Theoryの分厚い教科書を学習させて、数学論文の「モノマネ」をさせたもの。https://goo.gl/FGtFGS (グロタンディックをおちょくってるのかと思うけど、ま、面白いから許す。）

それはさておき、左側は見事に数学論文のマネをしているのだが、右側の上の方を見て欲しい。明らかに、diagramをマネる事に失敗している。ざまあみろだ。

Voevodskyがすごいのは、図１のような証明を、コンピュータにやらせるシステムを作ろうとしていた事。それは、この図を冒頭に掲げた彼の論文 "The Origins and Motivations of Univalent Foundations" https://goo.gl/3y79Zbを読めばわかる。

じゃ、Voevodskyは、論文やプロジェクターではなく、講義をする時には、どうしていたのだろう。

答えは、簡単である。

黒板にチョークで図を書いていたのである。

2011年ごろ、プリンストンの彼の講義のビデオをみて、ディジタル万歳の僕は、ちょっと軽いカルチャーショックを受けた。

でも、黒板とチョークの方が、合理的で効率的なのだ。間違っても、すぐ消せるし、すぐ直せる。横書きはできるけど、縦書きを混ぜることができないコンピュータで、行列や列ベクトルを書くのに、苦労しているのは、なんかおかしい。

Quantum Information Scienceのミーティング IT from Qbit にたくさんビデオが上がっているけど https://www.simonsfoundation.org/it…/it-from-qubit-meetings/ 黒板派が圧倒的に多い。