実は俺、そーゆープログラム作ろうかと思ってるんだよな。
準ウィキ方式で、わりと誰でも参加できるからデータ量けっこう楽に増えると思うし。
たとえばAはa1,a2,a3...といった性質を持ってて、Aであり、さらにbの性質を持つとBであるとか、まぁ完全な証明ができるわけじゃないけど道筋をたたき出す感じで。
A→Zを証明するとしたら、Aのa3の性質はZであるための絶対条件であるゆえにZとかを自動で叩き出す。
証明って今までに出された結果が効率的に使えてないから難しいと思うんだよね。だったらそこはコンピュータにやらせようと。