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 proven

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")

...Whoops. Yup, SMT solvers can famously return `unknown` on top of `sat` and `unsat`. Just added a post addendum about the mistake.