僕は、こんなソフトが欲しい！

数学の本を読んでたら、
This is trivial.（これは自明である）とか
The proof is omitted.（証明は省略する）
というのによく遭遇する。
また、証明は省略されていて、引用文献だけ紹介される場合もある。
１冊の本の中で、こういった証明の省略に、
何回も遭遇すると非常に疲れる。

そこで、こんな定理証明ソフトあったらいいと思う。
入力：命題（仮定と結論）
出力：真偽判定。真の場合は証明。偽の場合は反例。

インターフェースは、ノベルゲーム風。
個人的には、妹がお兄ちゃんに定理の証明を教えてくれる感じがいい。

証明できたら、「お兄ちゃん、こんなのも証明できないの？以下、証明」
命題が偽だったら、「お兄ちゃん、これ反例あるよ。以下、反例」
真偽判定できなかったら、「これ難しいね。私わからない」

プレイヤーの好みに合わせて、
生徒役(主人公)と教師役の性別やキャラを選べるとか。
一回証明させた問題を、穴抜きにして、トレーニング用のクイズを出してくれるとか。

これなら数学好きな人も増える。

そして、もしそんなソフトがあれば僕も欲しいけど、まだないですよね。とほほ。
いろいろ妄想とアイディアはあるんだけど、実装力が無さすぎて(涙)