We present a proof-producing integration of ACL2 and Imandra for proving nonlinear inequalities. This leverages a new Imandra interface exposing its nonlinear decision procedures. The reasoning takes place over the reals, but the proofs produced are valid over the rationals and may be run in both ACL2 and ACL2(r). The ACL2 proofs Imandra constructs are extracted from Positivstellensatz refutations, a real algebraic analogue of the Nullstellensatz, and are found using convex optimization.

翻译：我们提出了一种在ACL2与Imandra之间进行证明生成的集成方法，用于证明非线性不等式。该方法利用Imandra新接口暴露其非线性判定过程。推理过程在实数域上进行，但所生成的证明在有理数域上同样有效，且可在ACL2和ACL2(r)中运行。Imandra构建的ACL2证明从Positivstellensatz反证中提取（后者是Nullstellensatz在实代数域上的类似物），并通过凸优化技术求解。