Have the common algorithms in existing computer-assisted proofs been transitioned to proof assistants?

Question

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?

Answer 1

These tools are rather different in nature:

• Some (Coq?) assistants are able to solve SAT

• Some of these tasks can be done externally - e.g. verifying that one has a Groebner basis is much easier than actually computing it, so verification can be done internally in the assistant, and computation of it outsourced. However, Coq has Groebner bases for quite some time already.

• CAD is very hard in practice. Is verifying that one got CAD easier than computing it? (maybe).

• Convex inequalities - what exactly is the task? Verifying solvability seems easy (plug the solution in each inequality). Verifying non-solvability much less so (easier if strict duality holds, something that in general needs not to be the case).

• not sure about the last item, what is it, more details are needed.