> we already have "practical" NP problem solvers in classical silicon in the form of SMT solvers. They're out there, and practical for some problems, but SMT s

> we already have "practical" NP problem solvers in classical silicon in the form of SMT solvers. They're out there, and practical for some problems, but SMT solvers aren't exactly a solved problem. They're used for deductive proofs about program correctness, which are still pretty finicky. [0] [0] https://blog.adacore.com/using-spark-to-prove-255-bit-integer-arithmetic-from-curve25519 https://blog.adacore.com/using-spark-to-prove-255-bit-intege...