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 alpha link.

Answer 1

이것은 Z3의 대상 범위를 벗어납니다. 계승, 이항법에 대한 기본 지식은 없습니다. 지수에 대해 매우 제한된 추론을 수행합니다.

Answer 2

맥시마도 사실이라고 판단 할 수있는 것 같습니다. 맥시마는 신원을 많이 적용하고 다른 표현에 많은 합산을 줄일 수 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