z3を含む階乗を含む数学的ステートメントを証明することは可能ですか？

Question

私は、次の

ウォルフラムアルファは、それが証拠を提示していないが、それは確かにtrueであることを識別することができるように思われ、最大値は（何の驚きを決定することはできませんことを証明しようとしていますそこ）：

declare(n, integer) $ 
assume(n > 0) $ 
is(equals(2^n - n - 1 - sum(binomial(n,k), k, 2, n), 0)); 
=> unknown 

は、今私は）私はチュートリアルを行っているにもかかわらず、（私は大きな銃を引き出すとZ3をしようとするだろうと思ったが、私は階乗について、それを伝えようとしで捕まってしまいました。これらの種類の証拠はZ3のペイオードより高いですか？

編集：特定の問題は重要ではありません。私はこの問題の家族に対処できるツールを研究しようとしています。

EDIT2：固定のwolframアルファリンク。

Answer 1

これは、Z3が対象とする範囲の外にあります。 階乗、2項の組み込みの理解はありません。 指数に関する非常に限定された推論を実行します。

Answer 2

マキシマもそれが本当であると分かると思われます。 Maximaはアイデンティティの多くを適用し、他の式には多くの総和を減らすことができますsimplify_sumという名前のパッケージを持っている

sum(binomial(n,k),k,2,n),simpsum; 

Answer 3

試してみてください。

(%i65) load (simplify_sum); 
(%o65) /usr/share/maxima/5.39.0/share/solve_rec/simplify_sum.mac 
(%i66) simplify_sum (sum(binomial(n,k), k, 2, n)); 
        n 
(%o66)    2 - n - 1