投稿

Voevodsky と証明支援システム UniMath

先ごろ亡くなったVoevodsky(僕は「ヴォヴォスキー」と呼んでいたのだが、いい加減かもしれない)の仕事の一端を紹介しようと思う。 彼は、Milner予想、Bloch-Kato予想を解くなど、代数幾何でグロタンディックが進もうとした道で、大きな業績を残した。ヴォヴォスキーの最後の仕事は、数学の基礎とコンピュータに関係していた。 彼は、数学の証明に、コンピュータを使うべきだと主張した最初の数学者の一人で、また、そのためのコンピュータによる証明支援システムのライブラリーUniMthを開発した。 GitHub:  https://github.com/UniMath/UniMath 2016年9月の講演 "UniMath - a library of mathematics formalized in the univalent style"  https://goo.gl/3sJr1M 数学でのコンピュータの利用は、人工知能研究の重要な一分野だ。それは、ディープ・ラーニングや自然言語処理や検索技術とは、全く異なる技術が必要になる。 なぜ、数学の証明にコンピュータが必要なのか? かいつまんでいうと、こういうことだ。 フェルマーの定理を証明したワイルズが、謙遜して自分は「巨人の肩の上の小人だ」と言ったように、数学は、先行した無数の人たちの業績の蓄積の上に成り立っている。 もしも、ピタゴラスの子孫が生きていたとしても、ピタゴラスの定理を使うのに、彼らに著作権料を払う必要はない。また、その「証明」を自分で繰り返す必要はない。 ピタゴラスの「教団」は、いくつかの発見を「秘教」にしていたらしいのだが、少なくとも現代の数学では、情報の共有は、学問自体の前提でさえある。 ヴォヴォスキーは、興味ふかい経験をする。 2000年頃、彼は1993年に自分が発表した論文の重要な補題が間違っていたことに気づく。でも、その頃には、その論文は広く出回っていて、多くの数学者がその証明を「信じて」いた。彼が、その間違った補題なしでも、論文の結論が正しいことを証明できたのは、2006年になってからだった。 別のこともあった。1998年に共著で彼が発表した論文の証明に対して、「正しくない」という批判が出される。結論的には、彼は、正しかっ

「無言の誓い」-- Grothendiek, Lawvere and Voevodsky

グロタンディックに頼まれたカルボーニは、自分のアルファ・ロメオにローヴェールを乗せ、南仏の田舎のラベンダー畑の中のグロタンディックのボロ家に、彼を連れて行った。1989年のことだ。 2013年にカルボーニが亡くなった時、ローヴェールは、追悼文の中で、今まで知られてなかった事実を、初めて明かしている。 この時、グロタンディックはローヴェールに、自分が書きためた "Pursuing Stacks" の草稿の編集と出版を引き受けてもらおうとしていたというのだ。僕はローヴェールの「おっかけ」だったので、この「人選」は妥当なものだと思う。 (IT業界でたとえれば、ビル・ゲイツとスティーブ・ジョブスが、大事なビジネスの話で密会したようなもの) グロタンディック後期の代表的な論稿 "Pursuing Stacks" は、1983年頃に書かれたものだ。ただ、数学のアカデミーに背を向け田舎に隠棲していたグロタンディックのこの草稿の存在が広く知られるようになったのは、1990年代に入ってからだと思う。それは、草稿のコピーの形で人から人へと回覧された。 ローヴェールとグロタンディックの1989年の話に戻るが、面白いのは、この時、グロタンディックは、宗教的な「無言の誓い」の行の真っ最中で、話すことも数学について語ることも自分に禁じていたらしい。 人に頼みごとをしようとしていて、「無言の誓い」もないものだが、こんなすれ違いが起きるのは、グロタンディックの家には、電話がなかったからだと思う。(ビル・ゲイツが貧乏で、電話を止められていたと思えばいい。) でも、ローヴェールの突然の訪問が、嬉しくないわけはない。グロタンディックは、紙に "Bill !" と書いて、ローヴェールに示したという。 二人が会って数学の話をしないわけはない。数学については語らないというグロタンディックの誓いを、彼は自分で破ることになる。でも、しばらくは、筆談で数学の話をしたらしい。 最初から前途多難だが、まだ、続きがある。それについては、次回に。

Facebookのフェイク・ニュース対策?

イメージ
この投稿は元は、Facebookで行ったものだが、僕が引用したこのページ "Alien blog"   https://www.facebook.com/thealienblog/  は怪しいとFacebookは判断しているようだ。確かに、フェイク・ニュースてんこ盛りのページではある。 僕が、このページを引用したポストへの反応は、奇妙なものだった。反応がないわけではないが、いつもより極端に少ないのである。タグ付けした遠藤さんにさえ配信されてないことを知って、このポストにアクセス権限がかかっているらしいことに気づいた。 このビデオは、面白いものだったが、このサイトを宣伝するつもりはないので、Facebookのタイムラインからは、削除することにした。 ------- 僕のタイムラインに流れてきたビデオ。「殺人ロボット。それは、誰にも止められない。」 https://www.facebook.com/thealienblog/videos/1980805158908905/?hc_ref=ARQBTJcj57tnxfpmvoM5Sg6qlZ_2WrOvQdyvA3hw428NS3-qBz25F3lZZsvXITa1SCI 昔、角川アスキーのドローン好きの  遠藤 さんが、「ドローンは戦争を変えるかもしれない。」と言っていたのを思い出した。 映像を作ったのは、「宇宙人とUFO」という、かなりアレげなところなのだが、この映像はよく出来ている。一見の価値あり。 今、見に言ったら、この怪しいサイトの中でダントツによく観られている。僕のタイムラインにシェアしたのも、真面目なネパールの友人だった。 「誰にも止められない」というけど、鳥よけのネットとか、iPhoneの顔認証を破ったマスクのカカシとか、ハエたたきで防げるかも。 ま、あまり、ふざけない方がいいのかも。 船井 覚   これはうなされそうです いいね!  ·  返信  ·  昨日 11:14 管理する 長谷川 裕一   一個いくらかなぁ。何個か欲しいです(^^) いいね!  ·  返信  ·  1  ·  昨日 12:06 管理する

ごめんなさい。ありがとう。

イメージ
11/30マルレクの告知ページに誤りが。時間、17:00-20:00になっていましたが、19:00-21:00の間違いです。吉田 裕美さんが教えてくれました。吉田さん、ありがとうございます。 間違えた犯人は、もちろん、僕自身です。(なに、胸張ってるんじゃ。このボケが。) (もう直っていますが。以下、その顛末。) ところが、この間違い、主催者(僕のこと)じゃ修正できないんです。「日時」の変更できないんですね。(「開催場所」や「イベント名」の変更はできるんですが。なぜだろう?) 自分の間違いを棚に上げて、悪人の丸山は、「なんだこのクソ仕様」と一瞬思ったのですが、善人の丸山(というより、単に困った丸山)は、Peatixさんに泣きつくことにしました。 「案ずるより産むが易し」 (このたとえ、男が使っていいものかと、かねがね思っていたのですが)  「変更できます」  「て、て、手続きは、ど、どうすればいいのでしょう?」  「参加者に、時間変更のメッセージ送ってください」  「そ、そ、それだけですか? ぼ、ぼく、怪しい人かも」  「大丈夫です」  「???」 「溺れる者は藁をもつかむ」 (この人は、助かったんでしょうかね? 本人のセリフじゃなく、溺れる人をじっと観察している人がいたのでしょうか?)  でも、わかりました。 参加者にメッセージを送れるのは、主催者だけです。Peatixもメッセージのチェックは出来ますので、メッセージを送れという指示は、僕が主催者であることの認証に使えるんですね。 今見たら、もう修正終わってました。 ありがとうございます。Peatixの女の子。

Mac Book Airの引退と「丸山講演資料集」

2011年から、6年間使っていたMac Book Air が、現役引退しました。4Gのメモリーしかなく、最後の頃は少ないディスクも溢れて苦しかったのですが、よく頑張ってくれました。 年末に近づいていますね。ほっといていた「丸山 2017年 講演資料集」をまとめました。ご利用ください。 https://maruyama097.blogspot.com/2017/11/2017_15.html 末尾に 2016/2015/2014年の講演資料へのリンクを追加しました。ただ、それ以前のリンク作れていません。「Cloud研究会」時代の資料が抜けています。時々、自分で参照しているものがあるのですが ... 2011年以降のこれらのスライドは、全て、引退したMac Book Airで作られたものです。2万枚以上あると思います。 ご苦労様でした。

I walk on water

イメージ
Spotifyで歌詞が出るので、エミネムだって歌えるかもしれないと思っていた。彼の新曲 "I walk on water"  https://goo.gl/2VxDv5  がランクインしたので、さっそくやって見たが、あえなく敗退。 この曲は、彼にしてはそんなに早口ではない気がするのだが。舌が回らないのもあるのだが、歌詞を読んでも、すんなりとうまく訳せない。(Googleニューラル機械翻訳だってうまくいかないに決まっている) 何度か読んでるうちに(聴いては無理だった)、だんだん、自分のこと、自分の曲作りのことを歌っているのがわかってきたのだが。 ベラスケスやピカソが、絵を描く画家の絵を描いたのと同じだ。 よくわかったのは、ビヨンセが歌うメロディ・ラインの歌詞。  I walk on water  But I ain't no Jesus  I walk on water  But only when it freezes  'Cause I'm only human, just like you  ..... "only when it freezes" という歌詞を見た時、思わず吹き出したのだが、どんな感情でここを歌うのかと思うと、きっと笑うところではない気もする。 でも、聞き取れなかった最後の歌詞 "I wrote 'Stan' " を見て、少し、しびれる。この曲の「ラス・メニーナス」は、Stan だったんだ。 https://goo.gl/TbQFKq 歌を聴くのと、歌詞を読むのは、違うことだ。

働くママ × テクノロジー #01 人工知能と共存する未来の「はたらく」を考えよう

イメージ
今度の12月10日、「働くママ × テクノロジー #01 人工知能と共存する未来の「はたらく」を考えよう」というセミナーをやります。 https://goo.gl/dNG8nu 江頭 春可 さんのNarrativeBASE主催で、MaruLaboが協賛しています。興味のある方、ぜひ、ご参加ください。