8
$\begingroup$

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?

$\endgroup$
1

1 Answer 1

4
$\begingroup$

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.

$\endgroup$
4
  • $\begingroup$ 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? $\endgroup$ Feb 17, 2022 at 17:08
  • $\begingroup$ 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. $\endgroup$ Feb 17, 2022 at 17:15
  • 1
    $\begingroup$ Well, that's Mathematica for you, the best system (TM) in the Galaxy ;-) $\endgroup$ Feb 17, 2022 at 17:29
  • $\begingroup$ By the way, Groebner bases are in Coq since 2008 or so, see www-sop.inria.fr/marelle/personnel/Loic.Pottier/adg2008proc.pdf $\endgroup$ Feb 17, 2022 at 17:38

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.