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

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?

• I am not sufficiently expert to write a proper answer, but Lean has tactics like linarith (leanprover-community.github.io/mathlib_docs/…), and Buchberger's algorithm has also been implemented (matryoshka-project.github.io/pubs/dermitzakis_bsc_thesis.pdf) although that does not seem to have been incorporated in mathlib. Isabelle's sledgehammer is good at passing work to external solvers and translating their output into proofs that it can understand. Feb 17, 2022 at 15:22

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.

• If a system of complex polynomials is infeasible, then the Groebner basis I compute will be {1}. Are you saying that I can easily verify that {1} is a Groebner basis in such cases? Feb 17, 2022 at 17:08
• Ah, I think what you're saying is I can simply express 1 as a polynomial combination of the polynomials in my system. From what I can tell, such a certificate is not delivered by Mathematica, for example. Feb 17, 2022 at 17:15
• Well, that's Mathematica for you, the best system (TM) in the Galaxy ;-) Feb 17, 2022 at 17:29
• By the way, Groebner bases are in Coq since 2008 or so, see www-sop.inria.fr/marelle/personnel/Loic.Pottier/adg2008proc.pdf Feb 17, 2022 at 17:38