Wrote an article on solving my favorite number logic puzzle using a mixture of #Python and Microsoft Research's Z3: https://ahf.me/articles/2020/05/01/solving-binary-puzzles-using-python-and-z3/
Since then, played around with its optimizer a bit and found the API UX pretty lackluster: You can put in problems it doesn't support and rather than blow up, it will often just return non-optimal results.
As a makeshift CP solver, it does seem excellent though!
@ahf Probably not per se. As in, can't say SMT is something I've encountered regularly.
But as I'm sure you know, there's a huge market for optimization libraries in general, which Z3 ends up being a competitor in with its functionality (the AoC puzzle could also be solved with one of a billion LP solvers, but Z3 was way better; my own AoC solution used scipy.optimize and took 6 hours to run).
In the direction of theorem proving, I get the feel that Lean (also MS) is picking up a lot of speed.
Server run by the main developers of the project It is not focused on any particular niche interest - everyone is welcome as long as you follow our code of conduct!