Comment by zozbot234

> but I would usually rather see the full chain of steps directly for a proof in the published code instead of a semi-magic "by sledgehammer".

One issue with this is that coming up with a quickly-checkable certificate for UNSAT is not exactly a trivial problem. It's effectively the same as writing a formal proof.