多項式を微分すると指数が係数に出てくるのって，積の微分の公式 と を使って とかやると出てくる。ということに，多項式を計算機上でいじることについて考えていて初めて気付いた。

ぼくにとって，数学といえば積分らしい。それはきっと昔からそうで，ぼくにとって「積分」という言葉と積分記号は特別なものなのだろうと思う。例えば，あなたが誰かに向かって数学の話をしているところを想像して下さいと言われたら，黒板かホワイトボード…

Lean 本体 最初，github にあるソースを自分でコンパイルしようとしたらうまくいかなかった。apt-get で入るので始めからそうすればよかった。https://leanprover.github.io/download/ に環境ごとのインストールのしかたが書いてある。 Emacs の lean-mode E…