何がきっかけか忘れたのですが，一般に n 次元の重箱には隅が 2^(n-1) 個あるのだなということを思ったので，たいした話ではありませんが書いてみることにしました。n 次元重箱とは，n 次元立方体の境界から一つの側面の内部を除いた図形である。具体的には…

ある日の夜，寝ようとして布団に入った瞬間に，どういうわけか 676 という数字が浮かんできた。見覚えのある数字だ。でもどこで見たのだろうか。平方数か何かだろうか。そういえば 24 の二乗はそんな感じの数だった気がする。そこで計算してみると ，ちょっ…

掛け算記号の左右の役割は異なるので順番を入れ換えてはいけないという立場がある。左側は「一単位あたりいくつ」を表し，右側は「何単位分あるか」を表すのであり，それらを逆に書いてはいけないのだという。例えば，2×3=6 と書いたらそれは「三人がそれぞ…

先日 Coq 8.5 がリリースされたので入れてみた話。coq 自体のコンパイルは問題なくできたけど，その後 ssreflect のコンパイルに失敗した。make すると Error: The files /usr/local/lib/coq/parsing/pcoq.cmi and /usr/local/lib/coq/lib/compat.cmi make i…