>>455
この証明は証明自体もすごいけど、
そのツールがすごいんでしょ。
いわゆる微分とかの開発と似たような感じ。

だから、関心の対象になってる。
できたら理解してみたいけどなあ。時間ない。