nostr:nprofile1qy2hwumn8ghj7un9d3shjtnyd968gmewwp6kyqpqf3nlrmpjja65pzmvlegyl27l0y2m007nncxttdwqndrejajvdzasqj5wht SAT solvers are very complex, and would be even more complicated to prove them correct...
@nprofile1q... maybe the proof of the transform (that you already have in Lean) can be used to design that certificate? If the transform would emit the steps it did that follows the structure of the Lean proof....