Cutting Planes with Lean 4

by Bernardo Borges

This book is the official documentation for the usage of the lean-cutting-planes library. It is currently a work in progress, with the goal to provide full expressivity in Lean 4 for the cutting planes formal logic.

Future work in this project will aim to verify unsat demonstrations that were produced by solvers suchs as RoundingSat and check that their reasoning was correct.