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
by potato-peeler
2 subcomments
For the curious, solvers like z3 are used in programming languages to verify logic and constraints. Basically it can help find logic issues and bugs during compile time itself, instead of waiting for it to show up in runtime.
Hacker News