時間があるのか時間がないのか 誤解 全て誤解だ

あら、前回の記事から4か月経ってる。

ここまで間が空くと、
何を書いたら良いのかわからんもんですな。

とりあえず宣伝しなければならぬのは、
本を書きました。

 タイトル:Coq/SSReflect/MathCompによる定理証明 ~フリーソフトではじめる数学の形式化~
 出版社:森北出版
です。

コンピュータを使って定理を証明しちゃおう
って話です。

専門的な言葉で言うと
 SSReflectの入門書
的な位置づけです。

良かったら SSReflect本 って呼んでね。

出版社による公式HP(?)はここをクリックです。

表紙はこんな感じ。

可愛いでしょ。


映画は、あんまり観れてないのですが、
時々見てます。

最近観たものは
 ・ゲティ家の身代金
 ・サバービコン 仮面を被った街
 ・映画 プリキュアスーパースターズ!
 ・羊の木
 ・(チャップリンの)独裁者
 ・監獄の首領
 ・殺人者の記憶法
 ・静寂の森の凍えた姉妹
 ・x + y
 ・Too Young To Die
 ・NERVE/ナーヴ 世界で一番危険なゲーム
 ・スリー・ビルボード
 ・IT “それ”が見えたら、終わり。
 ・バリー・シール/アメリカをはめた男
 ・Battle of Sexes
 ・I, Tonya
 ・ガール・オン・ザ・トレイン
 ・グレイテスト・ショーマン
 ・嘘八百
です。
覚えている範囲です。
ちなみに、この順番は思い出した順です。


ドラマも観てます。
今年観たもの、観てるものは

 ・Nobel
 ・99.9-刑事専門弁護士- SEASONⅡ
 ・相棒
 ・コンフィデンスマンJP
 ・シグナル

くらいでしょうか。
どれも面白いです。
一番上のNobelは、海外ドラマで、日本と海外の違いを考えさせられる逸品です。
最下の2つは、現在(5月16日)も継続放送中です。気になる方は是非。

デンマークとスウェーデンで1月から放送が開始された The BRIDGE が観たいのですが、
日本での放送はいつからだろう。
観たら泣くだろうな。たぶん。泣く。そして、無力感・脱力感に襲われるだろうな。たぶん。


2018年、新年のご挨拶

明けましておめでとうございます。

萩原です。

「一年の計は元旦にあり」
の意味を勘違いしていました。
どう勘違いしていたかは内緒。

ちなみに正しい意味は
 1年の計画・目標は1月1日の朝のうちに立てましょう
です。

というわけで私の2018年の目標は
・趣味や興味のあることに時間を割く。
・数式をこねくりまわす技術を身につける。
・海外出張を充実させる。
・健康診断や人間ドックで悪いところが見つからないようになる。
です。

2018年もよろしくお願いします。


萩原研:研究集会参加・講演情報(11月下旬から12月上旬)

はっ!
ブログで全然研究の話をしていない。

ここらで、講演情報などを書かせて頂きます。


「実験計画法と符号および関連する組合せ構造」
11月23日~25日
神奈川県の湯河原温泉

萩原が2日目(24日)に
入門講義「挿入・削除符号へ誘う綺麗な性質」
を講演します。


「情報理論とその応用シンポジウム」
11月28日~12月1日
新潟県月岡温泉

萩原研からは3件:
29日:一般講演「バランス隣接挿入/削除誤りの性質」、萩原。
29日:一般講演「Binary Multipermutation Ulam Sphere Analysis」、Justin Kong、萩原。
29日:ワークショップ「符号理論の向こうへ 〜純粋数学や知的財産権〜」のオーガナイザを萩原。

特に、ワークショップは

講演者
北詰 正顕(千葉大学),中辻 史郎(中辻特許事務所)
要旨
このセッションでは,符号理論の拡がりをテーマとしています。符号理論に影響を受けて発展していく純粋数学という学術的側面,符号理論のアウトカムとしての知的財産権という産業的側面,それぞれを題材にしてご講演者の方々に講演頂く予定です。

というスペシャルなイベントになってます。


「Theorem Proving and Provers」
12月6日~7日
京都大学

萩原がTPPMarkに参加します。


「情報理論特別講演会」
12月8日
京都府烟河温泉

萩原研からは2件(うち、1件は、来年度配属予定の学生)
「Analysis of binary multipermutation spheres toward maximal code size lower bounds」、Justin Kong
「拡張したMean King問題を応用した量子鍵配送の検討と安全性」」、中山 歩(現:同志社大)