Coq

ついったで(Coq方面の)その筋の人らをフォローしてると、たまに「面白い証明を求む」とか、それくらいの証明じゃ面白くないとか、そういう呟きが流れてくることがある。

しかし、面白い証明っていったい何なの？
難しかったり、アクロバティックだったりすると面白いんだろうか？
めったに使わなさそうな難しい数学の概念とか証明すると面白いんだろうか？

面白いというのとちょっと違うけど、美しい証明について、論理学の矢田部先生がこんなこと述べてる。
http://ask.fm/ytb_at_twt/answer/113649001034

同様に面白い証明なんてものはない。とも言えるんじゃないかと思う。

そもそも、私のような初心者だと、n+0=nの証明とか足し算の交換法則の証明とかだけでも結構楽しいんですが。
テトリスやってるような感覚だし。レバガチャでも結構勝つるし。