In my experience, one of the most common applications of computer-assisted proofs in math is establishing that a given system of constraints is infeasible. Here are some examples of settings and tools in this vein:
- Boolean formula (by SAT solver)
- System of complex polynomial equations (by computing a Groebner basis)
- System of real polynomial equations and inequalities (by cylindrical algebraic decomposition)
- System of convex constraints (by convex programming)
- System of inequalities (by interval arithmetic and linear programming)
In each setting, one expects that the tool's logic could be systematically converted to a formalized proof.
To what extent have these tools been converted to formal proof writers?