Ist es möglich, mathematische Aussagen einschließlich Fakultäten mit z3 zu beweisen?

Question

Ich versuche, die folgende

Wolfram Alpha zu beweisen scheint in der Lage zu sein, zu erkennen, dass es in der Tat true ist, obwohl es keinen Beweis vorlegen, und Maxima können sich nicht entscheiden (keine Überraschungen dort):

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

Nun dachte ich, dass ich die großen Kanonen bringen würde und versuchen Z3 (auch wenn ich nur das Tutorial) getan haben, aber ich habe bei Versuch stecken es über factorials zu erzählen. Liegen diese Beweise über dem Z3-Gehalt von Z3?

EDIT: Das besondere Problem ist nicht wichtig. Ich versuche nur, die Werkzeuge zu erforschen, die mit dieser Problemfamilie umgehen können.

EDIT2: Fehler behoben.

Answer 1

Dies liegt weit außerhalb des Anwendungsbereichs von Z3. Es gibt kein integriertes Verständnis von Faktoren, Binomen. Es führt sehr begrenzte Argumentation über Exponenten.

Answer 2

Maxima scheint auch zu erkennen, dass es wahr ist. Versuchen

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

Answer 3

Maxima hat ein Paket namens simplify_sum, die eine Menge von Identitäten anwenden können und viele Additionen auf andere Ausdrücke reduzieren.

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