Can SMT solver like Z3 prove 1+2+...+n = n(n+1)/2?

The theorem 1+2+...+n = n(n+1)/2 seems to be provable by first translating it to CNFs and repeatedly applying resolution rules to them, as discussed in the introduction section of [1]. I believe this means the theorem is solvable by SMT solver like Z3.

However, I thought first-order logic cannot deal with these kind of problems, because "No first-order theory, however, has the strength to uniquely describe a structure with an infinite domain, such as the natural numbers or the real line." [2]

So, my questions are:

Can we use Z3 to prove the theorem?
If so, how to program the equation 1+2+...+n = n(n+1)/2 in Z3?

[1] Learning to Prove Theorems via Interacting with Proof Assistants
[2] https://en.wikipedia.org/wiki/First-order_logic#:~:text=First%2Dorder%20logic%20is%20the,%2C%20into%20first%2Dorder%20logic.

I tried using Z3 to solve it, but I couldn't figure out how to specify the formula "1+2+..+n" in Z3 in the first place.

Solution

You can express such theorems, but existing SMT solvers aren't strong enough to prove them out-of-the box, at least not for the time being. This is because SMT solvers do not do induction, and such claims require induction for their proofs.

To illustrate, this is how you'd write the theorem you want in z3's Python API:

from z3 import *

dummy = Int('dummy')
Sum = RecFunction("Sum", IntSort(), IntSort())
RecAddDefinition(Sum, [dummy], If(dummy == 0, 0, dummy + Sum(dummy-1)))

def P(n):
  return Sum(n) == n * (n+1) / 2

n = Int('n')
prove(P(n))

Alas, if you run this you'll see that z3 loops forever.

In certain cases, you can get away by posing the inductive argument yourself:

from z3 import *

dummy = Int('dummy')
Sum = RecFunction("Sum", IntSort(), IntSort())
RecAddDefinition(Sum, [dummy], If(dummy == 0, 0, dummy + Sum(dummy-1)))

def P(n):
  return Sum(n) == n * (n+1) / 2

s = Solver()

# Induction. Base case:
s.add(P(0))

# Inductive-step. Assert for `n`. Assert the negation for `n+1`, hoping for unsat answer.
n = Int('n')
s.add(P(n))
s.add(Not(P(n+1)))

print(s.check())

Alas, this loops forever as well. The tool is just not capable of handling the required step.

You can also try adding Sum as an uninterpreted function, add axioms about it, and see if you can use some patterns to push the proof through. Alas, none of these attempts are very satisfactory. Even if you get a proof, it'll be brittle.

Bottom line, SMT solvers don't do induction, at least not for the time being. But the SMTLib spec allows for recursive function definitions, which naturally require inductive reasoning capabilities. Perhaps things will get better in the future, with possible user annotations, helping the solver find the inductive invariant. But, as it stands in early 2023, if you want to prove such theorems, you need to use actual theorem-provers, such as Isabelle, Coq, Lean, ACL2, etc.; or systems like Dafny, why3, etc., which automate inductive proofs much better than SMT solvers themselves.