離散数学の授業で定理証明器のことをちょっと触れたいと思って、証明の例題に使っている上記命題をCoqで証明してみました。多分いろいろ上手くないと思うのだけれどもさらしてみます。 Require Import Classical. Require Import Arith. Require Import Omeg…

私が学生として通っていた某大学は比較的新しいものなのですが、それができたのは市からの熱烈な誘致活動の結果だそうです。その当時の市長たちが、「この市を発展させるには、企業にとって魅力があるものになることが大事。それには良質な労働力が必要。だ…

どうして日本の大学はアメリカの様にならないのか - As a Futurist...一応ランキングでは公立で30位以内に入ってくる大学にいますが、そんなに意識の高い学生なんてそうそういませんって。そりゃアイビーリーグに入ってくるような人たちは違うかもしれません…

というわけでGo!

数学者が「幾何学の起源」や「基礎論」を疑い、別の幾何学や不完全性定理を導きだしたように。 http://d.hatena.ne.jp/KGV/20081203#1228309384 なんかタイトルで終わってますが、まあそういうことです。元記事では枝葉末節の部分なのでどうでもよいのですが…

ProofWeb知らなかった。CoqとかIsabelleとかのような定理証明器をウェブ上で動かせます。インストールがいらないのでちょっと遊んでみるのに便利ですね。まあ、操作性では劣りますが。

必要な予備知識を最低限にした論文なのに査読に時間がかかるなぁとか思っていたのですが、査読を見たら山ほど間違いとか不自然な表現とかを指摘されていて、要するにそういうのをピックするのに時間を取らせてしまったようです。ごめんなさい、ごめんなさい…

Twitter / tri_iro: くそう、こんなことになるなら、もうちょっと真面目に書いておけ ... そりゃあ、普通でない論文だってたくさんありますし、どれが普通でない論文かは著者が決めるわけではないので…。いずれにしても、修士論文とジャーナルに出すための論…