2/26/2026 at 5:45:23 PM
I'm suspicious of the theorem proving example. I thought Z3 could fail to return sat or unsat, but he is assuming that if it's not sat the theorem must be provenby jeremysalwen
2/26/2026 at 6:33:25 PM
No I think it's fine. On another note, I have proven Fermat's Last Theorem with z3 using this setup :) and it goes faster if you reduce a variable called "timeout" for some reason! from z3 import *
s = Solver()
s.set("timeout", 600)
a = Int('a')
b = Int('b')
c = Int('c')
s.add(a > 0)
s.add(b > 0)
s.add(c > 0)
theorem = a ** 3 + b ** 3 != c ** 3
if s.check(Not(theorem)) == sat:
print(f"Counterexample: {s.model()}")
else:
print("Theorem true")by ymherklotz
2/26/2026 at 6:31:16 PM
...Whoops. Yup, SMT solvers can famously return `unknown` on top of `sat` and `unsat`. Just added a post addendum about the mistake.by hwayne