Chriswarbo: not that simple. Neither "Wikipedia-sized proof", nor the last 200TB proof take their size from just "variable assignment for a SAT solver". The siz

Chriswarbo: not that simple. Neither "Wikipedia-sized proof", nor the last 200TB proof take their size from just "variable assignment for a SAT solver". The size comes from "proof certificates" that SAT problem has no solution == effectively you need to provide a verifiable evidence that search did not find a solution. In positive cases, when solution exists, all the evidence you need, is indeed just an assignment for the variables.