a thoughtful web.
Good ideas and conversation. No ads, no tracking.   Login or Take a Tour!
comment
user-inactivated  ·  3934 days ago  ·  link  ·    ·  parent  ·  post: Math proof too large for humans to check

The proof is a reduction to a boolean satisfiability problem, then the output of a SAT solver. They could obtain a shorter proof, analogous to Appel and Haken's Four Color Theorem proof, by proving the SAT solver correct.