Можно ли доказать математические утверждения, в том числе факториалы с z3?

Question

Я не пытаюсь доказать следующее

Wolfram Alpha, кажется, чтобы быть в состоянии различить, что это действительно true, хотя он не представляет доказательства, и максимумы не могут решить (без сюрпризов есть):

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

Теперь я думал, что выведу большие пушки и попытаться Z3 (хотя я только сделал учебник), но я застрял в попытке сказать ему о факториалах. Являются ли эти доказательства выше платности Z3?

EDIT: Особая проблема не имеет значения. Я просто пытаюсь исследовать инструменты, которые могут справиться с этим семейством проблем.

EDIT2: Исправлена ​​ссылка на альфа-волфрам.

Answer 1

Это не входит в сферу применения Z3. Нет встроенного понимания факториалов, биномов. Он выполняет очень ограниченные рассуждения об экспонентах.

Answer 2

Maxima также, похоже, способен распознать, что это правда. Попробуйте

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

Answer 3

Maxima есть пакет под названием simplify_sum, который может применить много идентичностей и уменьшить много сложений других выражений.

(%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