A heuristic prover for real inequalities

Jeremy Avigad, Robert Y. Lewis, Cody Roux

We describe a general method for verifying inequalities between real-valued expressions, especially the kinds of straightforward inferences that arise in interactive theorem provin…