## Hilbert’s 10th problem, Fermat’s last theorem and SMT solvers

Hilbert's 10th problem states that you cannot devise an algorithm which can solve any diophantine equation over integers. However, it's important to understand, that this is possible over fixed-size bitvectors.

Fermat's last theorem states that there are no integer solution(s) for $a^n + b^n = c^n$, for $n>=3$.

Let's prove it for n=3 and for a in 0..255 range:

from z3 import *

# for a 8-bit bitvec, to prevent overflow during multiplication/addition, 25 bits must be allocated
# because log2(256)*3 = 8*3 = 24
# and a sum of two 24-bit bitvectors can be 25-bit
a,b,c = BitVecs ('a b c', 25)

s=Solver()

# only 8-bit values are allowed in these 3 bitvectors:

# non-zero values:

# a^3 + b^3 = c^3

print s.check()



Z3 gives "unsat", meaning, it couldn't find any a/b/c. However, this is possible to check even using brute-force search.

If to replace "BitVecs" by "Ints", Z3 would give "unknown":

from z3 import *

a,b,c = Ints ('a b c')

s=Solver()

# a^3 + b^3 = c^3